:: BINOM semantic presentation
:: deftheorem BINOM:def 1 :
canceled;
:: deftheorem BINOM:def 2 :
canceled;
:: deftheorem E1 defines add-cancelable BINOM:def 3 :
theorem E2: :: BINOM:1
theorem E3: :: BINOM:2
scheme :: BINOM:sch 1
s1{ F
1()
-> Nat, P
1[
Nat] } :
for b
1 being
Nat holds
( F
1()
<= b
1 implies P
1[b
1] )
E4:
P
1[F
1()]
and
E5:
for b
1 being
Nat holds
( ( F
1()
<= b
1 & P
1[b
1] ) implies ( P
1[b
1 + 1] ) )
proof
let c
1 be
Nat;
assume E6:
F
1()
<= c
1
;
defpred S
1[
Nat] means P
1[F
1()
+ a
1];
E7:
S
1[0]
by E4;
E8:
now
let c
2 be
Nat;
assume E9:
S
1[c
2]
;
F
1()
<= F
1()
+ c
2
by NAT_1:29;
then
P
1[
(F1() + c2) + 1]
by E5, E9;
hence
S
1[c
2 + 1]
;
end;
E9:
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E7, E8);
ex b
1 being
Nat st c
1 = F
1()
+ b
1
by E6, NAT_1:28;
hence
P
1[c
1]
by E9;
end;
scheme :: BINOM:sch 2
s2{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> Element of F
2(), F
4()
-> Function of
[:F1(),F2():],F
2() } :
ex b
1 being
Function of
[:NAT ,F1():],F
2() st
for b
2 being
Element of F
1() holds
( b
1 . 0,b
2 = F
3() & for b
3 being
Nat holds b
1 . (b3 + 1),b
2 = F
4()
. b
2,
(b1 . b3,b2) )
proof
E4:
for b
1 being
Element of F
1() holds
ex b
2 being
Function of
NAT ,F
2() st
( b
2 . 0
= F
3() & for b
3 being
Nat holds b
2 . (b3 + 1) = F
4()
. b
1,
(b2 . b3) )
proof
let c
1 be
Element of F
1();
defpred S
1[
Nat,
Element of F
2(),
Element of F
2()] means a
3 = F
4()
. c
1,a
2;
E5:
for b
1 being
Natfor b
2 being
Element of F
2() holds
ex b
3 being
Element of F
2() st
S
1[b
1,b
2,b
3]
;
ex b
1 being
Function of
NAT ,F
2() st
( b
1 . 0
= F
3() & for b
2 being
Element of
NAT holds
S
1[b
2,b
1 . b
2,b
1 . (b2 + 1)] )
from RECDEF_1:sch 2(E5);
hence
ex b
1 being
Function of
NAT ,F
2() st
( b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
1,
(b1 . b2) )
;
end;
ex b
1 being
Function of F
1(),
Funcs NAT ,F
2() st
for b
2 being
Element of F
1() holds
ex b
3 being
Function of
NAT ,F
2() st
( b
1 . b
2 = b
3 & b
3 . 0
= F
3() & for b
4 being
Nat holds b
3 . (b4 + 1) = F
4()
. b
2,
(b3 . b4) )
proof
set c
1 =
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) } ;
E5:
now
let c
2, c
3, c
4 be
set ;
assume E6:
(
[c2,c3] in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) } &
[c2,c4] in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) } )
;
then consider c
5 being
Element of F
1(), c
6 being
Element of
Funcs NAT ,F
2() such that
E7:
(
[c2,c3] = [c5,c6] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
6 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
5,
(b1 . b2) ) )
;
consider c
7 being
Function of
NAT ,F
2() such that
E8:
( c
7 = c
6 & c
7 . 0
= F
3() & for b
1 being
Nat holds c
7 . (b1 + 1) = F
4()
. c
5,
(c7 . b1) )
by E7;
consider c
8 being
Element of F
1(), c
9 being
Element of
Funcs NAT ,F
2() such that
E9:
(
[c2,c4] = [c8,c9] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
9 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
8,
(b1 . b2) ) )
by E6;
consider c
10 being
Function of
NAT ,F
2() such that
E10:
( c
10 = c
9 & c
10 . 0
= F
3() & for b
1 being
Nat holds c
10 . (b1 + 1) = F
4()
. c
8,
(c10 . b1) )
by E9;
E11: c
5 =
[c2,c3] `1
by E7, MCART_1:def 1
.=
c
2
by MCART_1:def 1
.=
[c8,c9] `1
by E9, MCART_1:def 1
.=
c
8
by MCART_1:def 1
;
E12:
(
NAT = dom c
7 &
NAT = dom c
10 )
by FUNCT_2:def 1;
E13:
now
let c
11 be
set ;
assume
c
11 in NAT
;
then reconsider c
12 = c
11 as
Nat ;
defpred S
1[
Nat] means c
7 . a
1 = c
10 . a
1;
E14:
S
1[0]
by E8, E10;
E15:
now
let c
13 be
Nat;
assume E16:
S
1[c
13]
;
c
7 . (c13 + 1) =
F
4()
. c
8,
(c7 . c13)
by E8, E11
.=
c
10 . (c13 + 1)
by E10, E16
;
hence
S
1[c
13 + 1]
;
end;
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E14, E15);
hence c
7 . c
11 =
c
10 . c
12
.=
c
10 . c
11
;
end;
thus c
3 =
[c5,c6] `2
by E7, MCART_1:def 2
.=
c
6
by MCART_1:def 2
.=
c
9
by E8, E10, E12, E13, FUNCT_1:9
.=
[c2,c4] `2
by E9, MCART_1:def 2
.=
c
4
by MCART_1:def 2
;
end;
now
let c
2 be
set ;
assume
c
2 in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) }
;
then consider c
3 being
Element of F
1(), c
4 being
Element of
Funcs NAT ,F
2() such that
E6:
( c
2 = [c3,c4] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
4 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
3,
(b1 . b2) ) )
;
thus
c
2 in [:F1(),(Funcs NAT ,F2()):]
by E6, ZFMISC_1:def 2;
end;
then
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) } c= [:F1(),(Funcs NAT ,F2()):]
by TARSKI:def 3;
then reconsider c
2 =
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . b1,(b3 . b4) ) } as
Relation of F
1(),
Funcs NAT ,F
2()
by RELSET_1:def 1;
E6:
for b
1 being
set holds
( b
1 in dom c
2 implies b
1 in F
1() )
;
for b
1 being
set holds
( b
1 in F
1() implies b
1 in dom c
2 )
then
dom c
2 = F
1()
by E6, TARSKI:2;
then reconsider c
3 = c
2 as
Function of F
1(),
Funcs NAT ,F
2()
by E5, FUNCT_1:def 1, FUNCT_2:def 1;
take
c
3
;
for b
1 being
Element of F
1() holds
ex b
2 being
Function of
NAT ,F
2() st
( c
3 . b
1 = b
2 & b
2 . 0
= F
3() & for b
3 being
Nat holds b
2 . (b3 + 1) = F
4()
. b
1,
(b2 . b3) )
proof
let c
4 be
Element of F
1();
dom c
3 = F
1()
by FUNCT_2:def 1;
then
[c4,(c3 . c4)] in c
3
by FUNCT_1:8;
then consider c
5 being
Element of F
1(), c
6 being
Element of
Funcs NAT ,F
2() such that
E7:
(
[c4,(c3 . c4)] = [c5,c6] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
6 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
5,
(b1 . b2) ) )
;
consider c
7 being
Function of
NAT ,F
2() such that
E8:
( c
7 = c
6 & c
7 . 0
= F
3() & for b
1 being
Nat holds c
7 . (b1 + 1) = F
4()
. c
5,
(c7 . b1) )
by E7;
E9: c
4 =
[c5,c6] `1
by E7, MCART_1:def 1
.=
c
5
by MCART_1:def 1
;
c
3 . c
4 =
[c5,c6] `2
by E7, MCART_1:def 2
.=
c
6
by MCART_1:def 2
;
hence
ex b
1 being
Function of
NAT ,F
2() st
( c
3 . c
4 = b
1 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. c
4,
(b1 . b2) )
by E8, E9;
end;
hence
for b
1 being
Element of F
1() holds
ex b
2 being
Function of
NAT ,F
2() st
( c
3 . b
1 = b
2 & b
2 . 0
= F
3() & for b
3 being
Nat holds b
2 . (b3 + 1) = F
4()
. b
1,
(b2 . b3) )
;
end;
then consider c
1 being
Function of F
1(),
Funcs NAT ,F
2() such that
E5:
for b
1 being
Element of F
1() holds
ex b
2 being
Function of
NAT ,F
2() st
( c
1 . b
1 = b
2 & b
2 . 0
= F
3() & for b
3 being
Nat holds b
2 . (b3 + 1) = F
4()
. b
1,
(b2 . b3) )
;
set c
2 =
{ [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) } ;
E6:
now
let c
3, c
4, c
5 be
set ;
assume E7:
(
[c3,c4] in { [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) } &
[c3,c5] in { [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) } )
;
then consider c
6 being
Nat, c
7 being
Element of F
1(), c
8 being
Element of F
2() such that
E8:
(
[c3,c4] = [[c6,c7],c8] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
7 & c
8 = b
1 . c
6 ) )
;
consider c
9 being
Nat, c
10 being
Element of F
1(), c
11 being
Element of F
2() such that
E9:
(
[c3,c5] = [[c9,c10],c11] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
10 & c
11 = b
1 . c
9 ) )
by E7;
E10:
[c6,c7] =
[c3,c4] `1
by E8, MCART_1:def 1
.=
c
3
by MCART_1:def 1
.=
[[c9,c10],c11] `1
by E9, MCART_1:def 1
.=
[c9,c10]
by MCART_1:def 1
;
then E11: c
6 =
[c9,c10] `1
by MCART_1:def 1
.=
c
9
by MCART_1:def 1
;
c
7 =
[c9,c10] `2
by E10, MCART_1:def 2
.=
c
10
by MCART_1:def 2
;
hence c
4 =
[c3,c5] `2
by E8, E9, E11, MCART_1:def 2
.=
c
5
by MCART_1:def 2
;
end;
now
let c
3 be
set ;
assume
c
3 in { [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) }
;
then consider c
4 being
Nat, c
5 being
Element of F
1(), c
6 being
Element of F
2() such that
E7:
( c
3 = [[c4,c5],c6] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
5 & c
6 = b
1 . c
4 ) )
;
[c4,c5] in [:NAT ,F1():]
by ZFMISC_1:def 2;
hence
c
3 in [:[:NAT ,F1():],F2():]
by E7, ZFMISC_1:def 2;
end;
then
{ [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) } c= [:[:NAT ,F1():],F2():]
by TARSKI:def 3;
then reconsider c
3 =
{ [[b1,b2],b3] where B is Nat, B is Element of F1(), B is Element of F2() : ex b1 being Function of NAT ,F2() st
( b4 = c1 . b2 & b3 = b4 . b1 ) } as
Relation of
[:NAT ,F1():],F
2()
by RELSET_1:def 1;
E7:
for b
1 being
set holds
( b
1 in dom c
3 implies b
1 in [:NAT ,F1():] )
;
for b
1 being
set holds
( b
1 in [:NAT ,F1():] implies b
1 in dom c
3 )
then
dom c
3 = [:NAT ,F1():]
by E7, TARSKI:2;
then reconsider c
4 = c
3 as
Function of
[:NAT ,F1():],F
2()
by E6, FUNCT_1:def 1, FUNCT_2:def 1;
take
c
4
;
for b
1 being
Element of F
1() holds
( c
4 . 0,b
1 = F
3() & for b
2 being
Nat holds c
4 . (b2 + 1),b
1 = F
4()
. b
1,
(c4 . b2,b1) )
proof
let c
5 be
Element of F
1();
consider c
6 being
Function of
NAT ,F
2() such that
E8:
( c
1 . c
5 = c
6 & c
6 . 0
= F
3() & for b
1 being
Nat holds c
6 . (b1 + 1) = F
4()
. c
5,
(c6 . b1) )
by E5;
[0,c5] in [:NAT ,F1():]
by ZFMISC_1:def 2;
then
[0,c5] in dom c
4
by FUNCT_2:def 1;
then consider c
7 being
set such that
E9:
[[0,c5],c7] in c
4
by RELAT_1:def 4;
consider c
8 being
Nat, c
9 being
Element of F
1(), c
10 being
Element of F
2() such that
E10:
(
[[0,c5],c7] = [[c8,c9],c10] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
9 & c
10 = b
1 . c
8 ) )
by E9;
consider c
11 being
Function of
NAT ,F
2() such that
E11:
( c
11 = c
1 . c
9 & c
10 = c
11 . c
8 )
by E10;
E12:
[0,c5] =
[[c8,c9],c10] `1
by E10, MCART_1:def 1
.=
[c8,c9]
by MCART_1:def 1
;
then E13: c
8 =
[0,c5] `1
by MCART_1:def 1
.=
0
by MCART_1:def 1
;
E14: c
7 =
[[c8,c9],c10] `2
by E10, MCART_1:def 2
.=
c
10
by MCART_1:def 2
;
E15: c
9 =
[0,c5] `2
by E12, MCART_1:def 2
.=
c
5
by MCART_1:def 2
;
E16: c
4 . 0,c
5 =
c
4 . [0,c5]
by BINOP_1:def 1
.=
F
3()
by E8, E9, E11, E13, E14, E15, FUNCT_1:8
;
now
let c
12 be
Nat;
[(c12 + 1),c5] in [:NAT ,F1():]
by ZFMISC_1:def 2;
then
[(c12 + 1),c5] in dom c
4
by FUNCT_2:def 1;
then consider c
13 being
set such that
E17:
[[(c12 + 1),c5],c13] in c
4
by RELAT_1:def 4;
consider c
14 being
Nat, c
15 being
Element of F
1(), c
16 being
Element of F
2() such that
E18:
(
[[(c12 + 1),c5],c13] = [[c14,c15],c16] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
15 & c
16 = b
1 . c
14 ) )
by E17;
consider c
17 being
Function of
NAT ,F
2() such that
E19:
( c
17 = c
1 . c
15 & c
16 = c
17 . c
14 )
by E18;
E20:
[(c12 + 1),c5] =
[[c14,c15],c16] `1
by E18, MCART_1:def 1
.=
[c14,c15]
by MCART_1:def 1
;
then E21: c
14 =
[(c12 + 1),c5] `1
by MCART_1:def 1
.=
c
12 + 1
by MCART_1:def 1
;
E22: c
13 =
[[c14,c15],c16] `2
by E18, MCART_1:def 2
.=
c
16
by MCART_1:def 2
;
E23: c
15 =
[(c12 + 1),c5] `2
by E20, MCART_1:def 2
.=
c
5
by MCART_1:def 2
;
[c12,c5] in [:NAT ,F1():]
by ZFMISC_1:def 2;
then
[c12,c5] in dom c
4
by FUNCT_2:def 1;
then consider c
18 being
set such that
E24:
[[c12,c5],c18] in c
4
by RELAT_1:def 4;
consider c
19 being
Nat, c
20 being
Element of F
1(), c
21 being
Element of F
2() such that
E25:
(
[[c12,c5],c18] = [[c19,c20],c21] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
1 . c
20 & c
21 = b
1 . c
19 ) )
by E24;
consider c
22 being
Function of
NAT ,F
2() such that
E26:
( c
22 = c
1 . c
20 & c
21 = c
22 . c
19 )
by E25;
E27:
[c12,c5] =
[[c19,c20],c21] `1
by E25, MCART_1:def 1
.=
[c19,c20]
by MCART_1:def 1
;
then E28: c
19 =
[c12,c5] `1
by MCART_1:def 1
.=
c
12
by MCART_1:def 1
;
E29: c
18 =
[[c19,c20],c21] `2
by E25, MCART_1:def 2
.=
c
21
by MCART_1:def 2
;
E30: c
20 =
[c12,c5] `2
by E27, MCART_1:def 2
.=
c
5
by MCART_1:def 2
;
thus c
4 . (c12 + 1),c
5 =
c
4 . [(c12 + 1),c5]
by BINOP_1:def 1
.=
c
6 . (c12 + 1)
by E8, E17, E19, E21, E22, E23, FUNCT_1:8
.=
F
4()
. c
5,c
21
by E8, E26, E28, E30
.=
F
4()
. c
5,
(c4 . [c12,c5])
by E24, E29, FUNCT_1:8
.=
F
4()
. c
5,
(c4 . c12,c5)
by BINOP_1:def 1
;
end;
hence
( c
4 . 0,c
5 = F
3() & for b
1 being
Nat holds c
4 . (b1 + 1),c
5 = F
4()
. c
5,
(c4 . b1,c5) )
by E16;
end;
hence
for b
1 being
Element of F
1() holds
( c
4 . 0,b
1 = F
3() & for b
2 being
Nat holds c
4 . (b2 + 1),b
1 = F
4()
. b
1,
(c4 . b2,b1) )
;
end;
scheme :: BINOM:sch 3
s3{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> Element of F
2(), F
4()
-> Function of
[:F2(),F1():],F
2() } :
ex b
1 being
Function of
[:F1(),NAT :],F
2() st
for b
2 being
Element of F
1() holds
( b
1 . b
2,0
= F
3() & for b
3 being
Nat holds b
1 . b
2,
(b3 + 1) = F
4()
. (b1 . b2,b3),b
2 )
proof
E4:
for b
1 being
Element of F
1() holds
ex b
2 being
Function of
NAT ,F
2() st
( b
2 . 0
= F
3() & for b
3 being
Nat holds b
2 . (b3 + 1) = F
4()
. (b2 . b3),b
1 )
proof
let c
1 be
Element of F
1();
defpred S
1[
Nat,
Element of F
2(),
Element of F
2()] means a
3 = F
4()
. a
2,c
1;
E5:
for b
1 being
Natfor b
2 being
Element of F
2() holds
ex b
3 being
Element of F
2() st
S
1[b
1,b
2,b
3]
;
ex b
1 being
Function of
NAT ,F
2() st
( b
1 . 0
= F
3() & for b
2 being
Element of
NAT holds
S
1[b
2,b
1 . b
2,b
1 . (b2 + 1)] )
from RECDEF_1:sch 2(E5);
hence
ex b
1 being
Function of
NAT ,F
2() st
( b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. (b1 . b2),c
1 )
;
end;
ex b
1 being
Function of F
1(),
Funcs NAT ,F
2() st
for b
2 being
Element of F
1() holds
ex b
3 being
Function of
NAT ,F
2() st
( b
1 . b
2 = b
3 & b
3 . 0
= F
3() & for b
4 being
Nat holds b
3 . (b4 + 1) = F
4()
. (b3 . b4),b
2 )
proof
set c
1 =
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . (b3 . b4),b1 ) } ;
E5:
now
let c
2, c
3, c
4 be
set ;
assume E6:
(
[c2,c3] in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . (b3 . b4),b1 ) } &
[c2,c4] in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . (b3 . b4),b1 ) } )
;
then consider c
5 being
Element of F
1(), c
6 being
Element of
Funcs NAT ,F
2() such that
E7:
(
[c2,c3] = [c5,c6] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
6 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. (b1 . b2),c
5 ) )
;
consider c
7 being
Function of
NAT ,F
2() such that
E8:
( c
7 = c
6 & c
7 . 0
= F
3() & for b
1 being
Nat holds c
7 . (b1 + 1) = F
4()
. (c7 . b1),c
5 )
by E7;
consider c
8 being
Element of F
1(), c
9 being
Element of
Funcs NAT ,F
2() such that
E9:
(
[c2,c4] = [c8,c9] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
9 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. (b1 . b2),c
8 ) )
by E6;
consider c
10 being
Function of
NAT ,F
2() such that
E10:
( c
10 = c
9 & c
10 . 0
= F
3() & for b
1 being
Nat holds c
10 . (b1 + 1) = F
4()
. (c10 . b1),c
8 )
by E9;
E11: c
5 =
[c2,c3] `1
by E7, MCART_1:def 1
.=
c
2
by MCART_1:def 1
.=
[c8,c9] `1
by E9, MCART_1:def 1
.=
c
8
by MCART_1:def 1
;
E12:
(
NAT = dom c
7 &
NAT = dom c
10 )
by FUNCT_2:def 1;
E13:
now
let c
11 be
set ;
assume
c
11 in NAT
;
then reconsider c
12 = c
11 as
Nat ;
defpred S
1[
Nat] means c
7 . a
1 = c
10 . a
1;
E14:
S
1[0]
by E8, E10;
E15:
now
let c
13 be
Nat;
assume E16:
S
1[c
13]
;
c
7 . (c13 + 1) =
F
4()
. (c7 . c13),c
8
by E8, E11
.=
c
10 . (c13 + 1)
by E10, E16
;
hence
S
1[c
13 + 1]
;
end;
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E14, E15);
hence c
7 . c
11 =
c
10 . c
12
.=
c
10 . c
11
;
end;
thus c
3 =
[c5,c6] `2
by E7, MCART_1:def 2
.=
c
6
by MCART_1:def 2
.=
c
9
by E8, E10, E12, E13, FUNCT_1:9
.=
[c2,c4] `2
by E9, MCART_1:def 2
.=
c
4
by MCART_1:def 2
;
end;
now
let c
2 be
set ;
assume
c
2 in { [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . (b3 . b4),b1 ) }
;
then consider c
3 being
Element of F
1(), c
4 being
Element of
Funcs NAT ,F
2() such that
E6:
( c
2 = [c3,c4] & ex b
1 being
Function of
NAT ,F
2() st
( b
1 = c
4 & b
1 . 0
= F
3() & for b
2 being
Nat holds b
1 . (b2 + 1) = F
4()
. (b1 . b2),c
3 ) )
;
thus
c
2 in [:F1(),(Funcs NAT ,F2()):]
by E6, ZFMISC_1:def 2;
end;
then
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4 + 1) = F4() . (b3 . b4),b1 ) } c= [:F1(),(Funcs NAT ,F2()):]
by TARSKI:def 3;
then reconsider c
2 =
{ [b1,b2] where B is Element of F1(), B is Element of Funcs NAT ,F2() : ex b1 being Function of NAT ,F2() st
( b3 = b2 & b3 . 0 = F3() & for b2 being Nat holds b3 . (b4<