Step | Hyp | Ref
| Expression |
1 | | cbvprod.2 |
. . . . . . . . . . . . . . 15
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![A A](_ca.gif) |
2 | 1 | nfcri 2276 |
. . . . . . . . . . . . . 14
![F/ F/](finv.gif) ![A A](_ca.gif) |
3 | | cbvprod.4 |
. . . . . . . . . . . . . 14
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![B B](_cb.gif) |
4 | | nfcv 2282 |
. . . . . . . . . . . . . 14
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![1
1](1.gif) |
5 | 2, 3, 4 | nfif 3505 |
. . . . . . . . . . . . 13
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) |
6 | | cbvprod.3 |
. . . . . . . . . . . . . . 15
![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![A A](_ca.gif) |
7 | 6 | nfcri 2276 |
. . . . . . . . . . . . . 14
![F/ F/](finv.gif) ![A A](_ca.gif) |
8 | | cbvprod.5 |
. . . . . . . . . . . . . 14
![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![C C](_cc.gif) |
9 | | nfcv 2282 |
. . . . . . . . . . . . . 14
![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![1
1](1.gif) |
10 | 7, 8, 9 | nfif 3505 |
. . . . . . . . . . . . 13
![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) |
11 | | eleq1w 2201 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | | cbvprod.1 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
13 | 11, 12 | ifbieq1d 3499 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 5, 10, 13 | cbvmpt 4031 |
. . . . . . . . . . . 12
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | | seqeq3 10254 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![n n](_n.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![n n](_n.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 16 | breq1i 3944 |
. . . . . . . . . 10
![seq seq](_seq.gif) ![n n](_n.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) |
18 | 17 | anbi2i 453 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![(
(](lp.gif) # ![seq
seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 18 | exbii 1585 |
. . . . . . . 8
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 19 | rexbii 2445 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) # ![seq
seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | seqeq3 10254 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 14, 21 | ax-mp 5 |
. . . . . . . 8
![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 22 | breq1i 3944 |
. . . . . . 7
![seq seq](_seq.gif) ![m m](_m.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) |
24 | 20, 23 | anbi12i 456 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | anbi2i 453 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | rexbii 2445 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 3, 8, 12 | cbvcsbw 3011 |
. . . . . . . . . . . 12
![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) |
28 | | ifeq1 3482 |
. . . . . . . . . . . 12
![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif)
![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k
k](_k.gif) ![]_ ]_](_urbrack.gif) ![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_
[_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) |
30 | 29 | mpteq2i 4023 |
. . . . . . . . . 10
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | seqeq3 10254 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . 9
![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 32 | fveq1i 5430 |
. . . . . . . 8
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) |
34 | 33 | eqeq2i 2151 |
. . . . . . 7
![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) |
35 | 34 | anbi2i 453 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif)
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 35 | exbii 1585 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 36 | rexbii 2445 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 26, 37 | orbi12i 754 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 38 | iotabii 5118 |
. 2
![( (](lp.gif) ![iota iota](riota.gif) ![x
x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![iota iota](riota.gif) ![x x](_x.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | | df-proddc 11352 |
. 2
![prod_ prod_](prod.gif)
![( (](lp.gif) ![iota iota](riota.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![j j](_j.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | | df-proddc 11352 |
. 2
![prod_ prod_](prod.gif)
![( (](lp.gif) ![iota iota](riota.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 39, 40, 41 | 3eqtr4i 2171 |
1
![prod_ prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) |