a1: for a being Element of F1() ex f being Function of NAT,F2() st
( f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) )
proof
let a be Element of F1(); :: thesis: ex f being Function of NAT,F2() st
( f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) )
defpred S1[ Nat, Element of F2(), Element of F2()] means $3 = F4($2,a,$1);
a2: for n being Nat
for x being Element of F2() ex y being Element of F2() st S1[n,x,y] ;
thus ex f being Function of NAT,F2() st
( f . 0 = F3() . a & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(a2); :: thesis: verum
end;
ex g being Function of F1(),(Funcs (NAT,F2())) st
for a being Element of F1() ex f being Function of NAT,F2() st
( g . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) )
proof
set h1 = { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } ;
a3: now :: thesis: for x, y1, y2 being object st [x,y1] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } & [x,y2] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } & [x,y2] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } implies y1 = y2 )
assume a4: ( [x,y1] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } & [x,y2] in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } ) ; :: thesis: y1 = y2
then consider a1 being Element of F1(), l1 being Element of Funcs (NAT,F2()) such that
a5: ( [x,y1] = [a1,l1] & ex f being Function of NAT,F2() st
( f = l1 & f . 0 = F3() . a1 & ( for n being Nat holds f . (n + 1) = F4((f . n),a1,n) ) ) ) ;
consider a2 being Element of F1(), l2 being Element of Funcs (NAT,F2()) such that
a6: ( [x,y2] = [a2,l2] & ex f being Function of NAT,F2() st
( f = l2 & f . 0 = F3() . a2 & ( for n being Nat holds f . (n + 1) = F4((f . n),a2,n) ) ) ) by a4;
consider f1 being Function of NAT,F2() such that
a7: ( f1 = l1 & f1 . 0 = F3() . a1 & ( for n being Nat holds f1 . (n + 1) = F4((f1 . n),a1,n) ) ) by a5;
consider f2 being Function of NAT,F2() such that
a8: ( f2 = l2 & f2 . 0 = F3() . a2 & ( for n being Nat holds f2 . (n + 1) = F4((f2 . n),a2,n) ) ) by a6;
a9: ( a1 = x & y1 = l1 & a2 = x & y2 = l2 ) by a5, a6, XTUPLE_0:1;
now :: thesis: for x being Element of NAT holds f1 . x = f2 . x
let x be Element of NAT ; :: thesis: f1 . x = f2 . x
defpred S1[ Nat] means f1 . $1 = f2 . $1;
a11: S1[ 0 ] by a7, a8, a9;
a12: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
then F4((f1 . n),a2,n) = f2 . (n + 1) by a8;
hence S1[n + 1] by a7, a9; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(a11, a12);
hence f1 . x = f2 . x ; :: thesis: verum
end;
hence y1 = y2 by a7, a8, a9, FUNCT_2:63; :: thesis: verum
end;
now :: thesis: for x being object st x in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } holds
x in [:F1(),(Funcs (NAT,F2())):]
let x be object ; :: thesis: ( x in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } implies x in [:F1(),(Funcs (NAT,F2())):] )
assume x in { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } ; :: thesis: x in [:F1(),(Funcs (NAT,F2())):]
then ex a being Element of F1() ex l being Element of Funcs (NAT,F2()) st
( x = [a,l] & ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) ) ;
hence x in [:F1(),(Funcs (NAT,F2())):] by ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider h1 = { [a,l] where a is Element of F1(), l is Element of Funcs (NAT,F2()) : ex f being Function of NAT,F2() st
( f = l & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) } as Relation of F1(),(Funcs (NAT,F2())) by TARSKI:def 3;
for x being object st x in F1() holds
x in dom h1
proof
let x be object ; :: thesis: ( x in F1() implies x in dom h1 )
assume x in F1() ; :: thesis: x in dom h1
then reconsider x1 = x as Element of F1() ;
consider f being Function of NAT,F2() such that
a15: ( f . 0 = F3() . x & ( for n being Nat holds f . (n + 1) = F4((f . n),x1,n) ) ) by a1;
reconsider f = f as Element of Funcs (NAT,F2()) by FUNCT_2:8;
[x,f] in h1 by a15;
hence x in dom h1 by XTUPLE_0:def 12; :: thesis: verum
end;
then F1() c= dom h1 ;
then dom h1 = F1() by XBOOLE_0:def 10;
then reconsider h1 = h1 as Function of F1(),(Funcs (NAT,F2())) by a3, FUNCT_1:def 1, FUNCT_2:def 1;
take h1 ; :: thesis: for a being Element of F1() ex f being Function of NAT,F2() st
( h1 . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) )
thus for a being Element of F1() ex f being Function of NAT,F2() st
( h1 . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) :: thesis: verum
proof
let a be Element of F1(); :: thesis: ex f being Function of NAT,F2() st
( h1 . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) )
dom h1 = F1() by FUNCT_2:def 1;
then [a,(h1 . a)] in h1 by FUNCT_1:1;
then consider x being Element of F1(), l being Element of Funcs (NAT,F2()) such that
a16: ( [a,(h1 . a)] = [x,l] & ex h being Function of NAT,F2() st
( h = l & h . 0 = F3() . x & ( for n being Nat holds h . (n + 1) = F4((h . n),x,n) ) ) ) ;
( a = x & h1 . a = l ) by a16, XTUPLE_0:1;
hence ex f being Function of NAT,F2() st
( h1 . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) by a16; :: thesis: verum
end;
end;
then consider g being Function of F1(),(Funcs (NAT,F2())) such that
a17: for a being Element of F1() ex f being Function of NAT,F2() st
( g . a = f & f . 0 = F3() . a & ( for n being Nat holds f . (n + 1) = F4((f . n),a,n) ) ) ;
set h1 = { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } ;
a18: now :: thesis: for x, y1, y2 being object st [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } implies y1 = y2 )
assume a19: ( [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } ) ; :: thesis: y1 = y2
then consider n1 being Element of NAT , a1 being Element of F1(), z1 being Element of F2() such that
a20: ( [x,y1] = [[a1,n1],z1] & ex f1 being Function of NAT,F2() st
( f1 = g . a1 & z1 = f1 . n1 ) ) ;
consider n2 being Element of NAT , a2 being Element of F1(), z2 being Element of F2() such that
a21: ( [x,y2] = [[a2,n2],z2] & ex f2 being Function of NAT,F2() st
( f2 = g . a2 & z2 = f2 . n2 ) ) by a19;
( x = [a1,n1] & x = [a2,n2] ) by a20, a21, XTUPLE_0:1;
then ( a1 = a2 & n1 = n2 ) by XTUPLE_0:1;
hence y1 = y2 by a20, a21, XTUPLE_0:1; :: thesis: verum
end;
now :: thesis: for x being object st x in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } holds
x in [:[:F1(),NAT:],F2():]
let x be object ; :: thesis: ( x in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } implies x in [:[:F1(),NAT:],F2():] )
assume x in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } ; :: thesis: x in [:[:F1(),NAT:],F2():]
then consider n1 being Element of NAT , a1 being Element of F1(), z1 being Element of F2() such that
a22: x = [[a1,n1],z1] and
ex f1 being Function of NAT,F2() st
( f1 = g . a1 & z1 = f1 . n1 ) ;
[a1,n1] in [:F1(),NAT:] by ZFMISC_1:def 2;
hence x in [:[:F1(),NAT:],F2():] by a22, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider h1 = { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of F2() : ex f being Function of NAT,F2() st
( f = g . a & z = f . n ) } as Relation of [:F1(),NAT:],F2() by TARSKI:def 3;
for x being object st x in [:F1(),NAT:] holds
x in dom h1
proof
let x be object ; :: thesis: ( x in [:F1(),NAT:] implies x in dom h1 )
assume x in [:F1(),NAT:] ; :: thesis: x in dom h1
then consider d, n being object such that
a24: ( d in F1() & n in NAT & x = [d,n] ) by ZFMISC_1:def 2;
reconsider d = d as Element of F1() by a24;
reconsider n = n as Element of NAT by a24;
consider h being Function of NAT,F2() such that
a25: g . d = h and
( h . 0 = F3() . d & ( for n being Nat holds h . (n + 1) = F4((h . n),d,n) ) ) by a17;
h . n is Element of F2() ;
then consider z being Element of F2() such that
a26: ex f being Function of NAT,F2() st
( f = g . d & z = f . n ) by a25;
[x,z] in h1 by a24, a26;
hence x in dom h1 by XTUPLE_0:def 12; :: thesis: verum
end;
then d2: [:F1(),NAT:] c= dom h1 ;
then dom h1 = [:F1(),NAT:] by XBOOLE_0:def 10;
then reconsider h1 = h1 as Function of [:F1(),NAT:],F2() by a18, FUNCT_1:def 1, FUNCT_2:def 1;
take h1 ; :: thesis: for a being Element of F1() holds
( h1 . (a,0) = F3() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F4((h1 . (a,n)),a,n) ) )
thus for a being Element of F1() holds
( h1 . (a,0) = F3() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F4((h1 . (a,n)),a,n) ) ) :: thesis: verum
proof
let a be Element of F1(); :: thesis: ( h1 . (a,0) = F3() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F4((h1 . (a,n)),a,n) ) )
consider h being Function of NAT,F2() such that
a27: ( g . a = h & h . 0 = F3() . a & ( for n being Nat holds h . (n + 1) = F4((h . n),a,n) ) ) by a17;
a28: now :: thesis: for k being Nat holds h1 . (a,(k + 1)) = F4((h1 . (a,k)),a,k)
let k be Nat; :: thesis: h1 . (a,(k + 1)) = F4((h1 . (a,k)),a,k)
[a,(k + 1)] in [:F1(),NAT:] by ZFMISC_1:def 2;
then [a,(k + 1)] in dom h1 by FUNCT_2:def 1;
then consider u being object such that
a29: [[a,(k + 1)],u] in h1 by XTUPLE_0:def 12;
k in NAT by ORDINAL1:def 12;
then [a,k] in [:F1(),NAT:] by ZFMISC_1:def 2;
then [a,k] in dom h1 by FUNCT_2:def 1;
then consider v being object such that
a30: [[a,k],v] in h1 by XTUPLE_0:def 12;
consider n1 being Element of NAT , d1 being Element of F1(), z1 being Element of F2() such that
a31: ( [[a,k],v] = [[d1,n1],z1] & ex f2 being Function of NAT,F2() st
( f2 = g . d1 & z1 = f2 . n1 ) ) by a30;
consider f2 being Function of NAT,F2() such that
a32: ( f2 = g . d1 & z1 = f2 . n1 ) by a31;
consider n being Element of NAT , d being Element of F1(), z being Element of F2() such that
a33: ( [[a,(k + 1)],u] = [[d,n],z] & ex f1 being Function of NAT,F2() st
( f1 = g . d & z = f1 . n ) ) by a29;
( [a,k] = [d1,n1] & [a,(k + 1)] = [d,n] ) by a31, a33, XTUPLE_0:1;
then a34: ( a = d1 & k = n1 & a = d & k + 1 = n ) by XTUPLE_0:1;
hence h1 . (a,(k + 1)) = h . n by a27, a29, a33, FUNCT_1:1
.= F4((f2 . n1),a,n1) by a27, a32, a34
.= F4((h1 . (a,k)),a,k) by a30, a32, a31, a34, FUNCT_1:1 ;
:: thesis: verum
end;
[a,0] in [:F1(),NAT:] by ZFMISC_1:def 2;
then consider u being object such that
a36: [[a,0],u] in h1 by d2, XTUPLE_0:def 12;
consider n being Element of NAT , d being Element of F1(), z being Element of F2() such that
a37: ( [[a,0],u] = [[d,n],z] & ex f1 being Function of NAT,F2() st
( f1 = g . d & z = f1 . n ) ) by a36;
( [a,0] = [d,n] & u = z ) by a37, XTUPLE_0:1;
then ( a = d & 0 = n ) by XTUPLE_0:1;
hence ( h1 . (a,0) = F3() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F4((h1 . (a,n)),a,n) ) ) by a27, a28, a36, a37, FUNCT_1:1; :: thesis: verum
end;