defpred S1[ set , set ] means ex f being Function of NAT,REAL st
( $2 = f & f . 0 = F2() . $1 & ( for n being Nat holds f . (n + 1) = F3((f . n),$1,n) ) );
c1: for a being Element of F1() ex f being Element of Funcs (NAT,REAL) st S1[a,f]
proof
let a be Element of F1(); :: thesis: ex f being Element of Funcs (NAT,REAL) st S1[a,f]
defpred S2[ Nat, set , set ] means $3 = F3($2,a,$1);
c2: for n being Nat
for x being Element of REAL ex y being Element of REAL st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of REAL ex y being Element of REAL st S2[n,x,y]
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S2[n,x,y]
reconsider y = F3(x,a,n) as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S2[n,x,y]
thus S2[n,x,y] ; :: thesis: verum
end;
reconsider A = F2() . a as Element of REAL ;
consider f being Function of NAT,REAL such that
c3: ( f . 0 = A & ( for n being Nat holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(c2);
 reconsider f = f as Element of Funcs (NAT,REAL) by FUNCT_2:8;
take f ; :: thesis: S1[a,f]
thus S1[a,f] by c3; :: thesis: verum
end;
consider g being Function of F1(),(Funcs (NAT,REAL)) such that
a17: for a being Element of F1() holds S1[a,g . a] from FUNCT_2:sch 3(c1);
 set h1 = { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL 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 REAL such that
a20: ( [x,y1] = [[a1,n1],z1] & ex f1 being Function of NAT,REAL st
( f1 = g . a1 & z1 = f1 . n1 ) ) ;
consider n2 being Element of NAT , a2 being Element of F1(), z2 being Element of REAL such that
a21: ( [x,y2] = [[a2,n2],z2] & ex f2 being Function of NAT,REAL 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 REAL : ex f being Function of NAT,REAL st
( f = g . a & z = f . n ) } holds
x in [:[:F1(),NAT:],REAL:]
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 REAL : ex f being Function of NAT,REAL st
( f = g . a & z = f . n ) } implies x in [:[:F1(),NAT:],REAL:] )
assume x in { [[a,n],z] where n is Element of NAT , a is Element of F1(), z is Element of REAL : ex f being Function of NAT,REAL st
( f = g . a & z = f . n ) } ; :: thesis: x in [:[:F1(),NAT:],REAL:]
then consider n1 being Element of NAT , a1 being Element of F1(), z1 being Element of REAL such that
a22: x = [[a1,n1],z1] and
ex f1 being Function of NAT,REAL st
( f1 = g . a1 & z1 = f1 . n1 ) ;
[a1,n1] in [:F1(),NAT:] by ZFMISC_1:def 2;
hence x in [:[:F1(),NAT:],REAL:] 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 REAL : ex f being Function of NAT,REAL st
( f = g . a & z = f . n ) } as Relation of [:F1(),NAT:],REAL 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,REAL such that
a25: g . d = h and
h . 0 = F2() . d and
for n being Nat holds h . (n + 1) = F3((h . n),d,n) by a17;
h . n is Element of REAL ;
then consider z being Element of REAL such that
a26: ex f being Function of NAT,REAL 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:],REAL by a18, FUNCT_1:def 1, FUNCT_2:def 1;
take h1 ; :: thesis: for a being Element of F1() holds
( h1 . (a,0) = F2() . a & ( for n being natural number holds h1 . (a,(n + 1)) = F3((h1 . (a,n)),a,n) ) )
thus for a being Element of F1() holds
( h1 . (a,0) = F2() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F3((h1 . (a,n)),a,n) ) ) :: thesis: verum
proof
let a be Element of F1(); :: thesis: ( h1 . (a,0) = F2() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F3((h1 . (a,n)),a,n) ) )
consider h being Function of NAT,REAL such that
a27: ( g . a = h & h . 0 = F2() . a & ( for n being Nat holds h . (n + 1) = F3((h . n),a,n) ) ) by a17;
a28: now :: thesis: for k being Nat holds h1 . (a,(k + 1)) = F3((h1 . (a,k)),a,k)
let k be Nat; :: thesis: h1 . (a,(k + 1)) = F3((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 REAL such that
a31: ( [[a,k],v] = [[d1,n1],z1] & ex f2 being Function of NAT,REAL st
( f2 = g . d1 & z1 = f2 . n1 ) ) by a30;
consider f2 being Function of NAT,REAL 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 REAL such that
a33: ( [[a,(k + 1)],u] = [[d,n],z] & ex f1 being Function of NAT,REAL 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
.= F3((f2 . n1),a,n1) by a27, a32, a34
.= F3((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 REAL such that
a37: ( [[a,0],u] = [[d,n],z] & ex f1 being Function of NAT,REAL 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) = F2() . a & ( for n being Nat holds h1 . (a,(n + 1)) = F3((h1 . (a,n)),a,n) ) ) by a27, a28, a36, a37, FUNCT_1:1; :: thesis: verum
end;