A1: for a being Element of F₁() ex f being Function of NAT ,F₂() st
( f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )

proof

let a be Element of F₁(); :: thesis: ex f being Function of NAT ,F₂() st
( f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )
defpred S₁[ Element of NAT , Element of F₂(), Element of F₂()] means $3 = F₄() . $2,a;
A2: for n being Element of NAT
for x being Element of F₂() ex y being Element of F₂() st S₁[n,x,y] ;
ex f being Function of NAT ,F₂() st
( f . 0 = F₃() & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
hence ex f being Function of NAT ,F₂() st
( f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) ; :: thesis: verum

end;

ex g being Function of F₁(),(Funcs NAT ,F₂()) st
for a being Element of F₁() ex f being Function of NAT ,F₂() st
( g . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )

proof

set h = { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } ;

A3: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } & [x,y2] in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } implies y1 = y2 )
assume that
A4: [x,y1] in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } and
A5: [x,y2] in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } ; :: thesis: y1 = y2
consider a1 being Element of F₁(), l1 being Element of Funcs NAT ,F₂() such that
A6: [x,y1] = [a1,l1] and
A7: ex f being Function of NAT ,F₂() st
( f = l1 & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a1 ) ) by A4;
consider a2 being Element of F₁(), l2 being Element of Funcs NAT ,F₂() such that
A8: [x,y2] = [a2,l2] and
A9: ex f being Function of NAT ,F₂() st
( f = l2 & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a2 ) ) by A5;
consider f1 being Function of NAT ,F₂() such that
A10: f1 = l1 and
A11: f1 . 0 = F₃() and
A12: for n being Element of NAT holds f1 . (n + 1) = F₄() . (f1 . n),a1 by A7;
consider f2 being Function of NAT ,F₂() such that
A13: f2 = l2 and
A14: f2 . 0 = F₃() and
A15: for n being Element of NAT holds f2 . (n + 1) = F₄() . (f2 . n),a2 by A9;
A16: a1 = [x,y1] `1 by A6, MCART_1:def 1
.= x by MCART_1:def 1
.= [a2,l2] `1 by A8, MCART_1:def 1
.= a2 by MCART_1:def 1 ;

A17: now

defpred S₁[ Element of NAT ] means f1 . $1 = f2 . $1;
let x be set ; :: thesis: ( x in NAT implies f1 . x = f2 . x )
assume x in NAT ; :: thesis: f1 . x = f2 . x
then reconsider x9 = x as Element of NAT ;

A18: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A19: S₁[n] ; :: thesis: S₁[n + 1]
f1 . (n + 1) = F₄() . (f1 . n),a2 by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A20: S₁[ 0 ] by A11, A14;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A20, A18);
hence f1 . x = f2 . x9
.= f2 . x ;
:: thesis: verum

end;

A21: ( NAT = dom f1 & NAT = dom f2 ) by FUNCT_2:def 1;
thus y1 = [a1,l1] `2 by A6, MCART_1:def 2
.= l1 by MCART_1:def 2
.= l2 by A10, A13, A21, A17, FUNCT_1:9
.= [x,y2] `2 by A8, MCART_1:def 2
.= y2 by MCART_1:def 2 ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } implies x in [:F₁(),(Funcs NAT ,F₂()):] )
assume x in { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } ; :: thesis: x in [:F₁(),(Funcs NAT ,F₂()):]
then ex a being Element of F₁() ex l being Element of Funcs NAT ,F₂() st
( x = [a,l] & ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) ) ;
hence x in [:F₁(),(Funcs NAT ,F₂()):] by ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider h = { [a,l] where a is Element of F₁(), l is Element of Funcs NAT ,F₂() : ex f being Function of NAT ,F₂() st
( f = l & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) } as Relation of F₁(),(Funcs NAT ,F₂()) by TARSKI:def 3;
A22: for x being set st x in F₁() holds
x in dom h

proof

let x be set ; :: thesis: ( x in F₁() implies x in dom h )
assume A23: x in F₁() ; :: thesis: x in dom h
then consider f being Function of NAT ,F₂() such that
A24: ( f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),x ) ) by A1;
reconsider f9 = f as Element of Funcs NAT ,F₂() by FUNCT_2:11;
[x,f9] in h by A23, A24;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set st x in dom h holds
x in F₁() ;
then dom h = F₁() by A22, TARSKI:2;
then reconsider h = h as Function of F₁(),(Funcs NAT ,F₂()) by A3, FUNCT_1:def 1, FUNCT_2:def 1;
take h ; :: thesis: for a being Element of F₁() ex f being Function of NAT ,F₂() st
( h . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )
for a being Element of F₁() ex f being Function of NAT ,F₂() st
( h . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )

proof

let a be Element of F₁(); :: thesis: ex f being Function of NAT ,F₂() st
( h . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) )
dom h = F₁() by FUNCT_2:def 1;
then [a,(h . a)] in h by FUNCT_1:8;
then consider a9 being Element of F₁(), l being Element of Funcs NAT ,F₂() such that
A25: [a,(h . a)] = [a9,l] and
A26: ex f9 being Function of NAT ,F₂() st
( f9 = l & f9 . 0 = F₃() & ( for n being Element of NAT holds f9 . (n + 1) = F₄() . (f9 . n),a9 ) ) ;
A27: h . a = [a9,l] `2 by A25, MCART_1:def 2
.= l by MCART_1:def 2 ;
a = [a9,l] `1 by A25, MCART_1:def 1
.= a9 by MCART_1:def 1 ;
hence ex f being Function of NAT ,F₂() st
( h . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) by A26, A27; :: thesis: verum

end;

hence for a being Element of F₁() ex f being Function of NAT ,F₂() st
( h . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) ; :: thesis: verum

end;

then consider g being Function of F₁(),(Funcs NAT ,F₂()) such that
A28: for a being Element of F₁() ex f being Function of NAT ,F₂() st
( g . a = f & f . 0 = F₃() & ( for n being Element of NAT holds f . (n + 1) = F₄() . (f . n),a ) ) ;
set h = { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } ;

A29: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } implies y1 = y2 )
assume that
A30: [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } and
A31: [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } ; :: thesis: y1 = y2
consider n1 being Element of NAT , a1 being Element of F₁(), z1 being Element of F₂() such that
A32: [x,y1] = [[a1,n1],z1] and
A33: ex f1 being Function of NAT ,F₂() st
( f1 = g . a1 & z1 = f1 . n1 ) by A30;
consider n2 being Element of NAT , a2 being Element of F₁(), z2 being Element of F₂() such that
A34: [x,y2] = [[a2,n2],z2] and
A35: ex f2 being Function of NAT ,F₂() st
( f2 = g . a2 & z2 = f2 . n2 ) by A31;
A36: [a1,n1] = [x,y1] `1 by A32, MCART_1:def 1
.= x by MCART_1:def 1
.= [[a2,n2],z2] `1 by A34, MCART_1:def 1
.= [a2,n2] by MCART_1:def 1 ;
then A37: n1 = [a2,n2] `2 by MCART_1:def 2
.= n2 by MCART_1:def 2 ;
a1 = [a2,n2] `1 by A36, MCART_1:def 1
.= a2 by MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A32, A33, A34, A35, A37, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } implies x in [:[:F₁(),NAT :],F₂():] )
assume x in { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } ; :: thesis: x in [:[:F₁(),NAT :],F₂():]
then consider n1 being Element of NAT , a1 being Element of F₁(), z1 being Element of F₂() such that
A38: x = [[a1,n1],z1] and
ex f1 being Function of NAT ,F₂() st
( f1 = g . a1 & z1 = f1 . n1 ) ;
[a1,n1] in [:F₁(),NAT :] by ZFMISC_1:def 2;
hence x in [:[:F₁(),NAT :],F₂():] by A38, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider h = { [[a,n],z] where n is Element of NAT , a is Element of F₁(), z is Element of F₂() : ex f being Function of NAT ,F₂() st
( f = g . a & z = f . n ) } as Relation of [:F₁(),NAT :],F₂() by TARSKI:def 3;
A39: for x being set st x in [:F₁(),NAT :] holds
x in dom h

proof

let x be set ; :: thesis: ( x in [:F₁(),NAT :] implies x in dom h )
assume x in [:F₁(),NAT :] ; :: thesis: x in dom h
then consider d, n being set such that
A40: d in F₁() and
A41: n in NAT and
A42: x = [d,n] by ZFMISC_1:def 2;
reconsider d = d as Element of F₁() by A40;
reconsider n = n as Element of NAT by A41;
consider f9 being Function of NAT ,F₂() such that
A43: g . d = f9 and
f9 . 0 = F₃() and
for n being Element of NAT holds f9 . (n + 1) = F₄() . (f9 . n),d by A28;
ex z being Element of F₂() ex f being Function of NAT ,F₂() st
( f = g . d & z = f . n )

proof

take f9 . n ; :: thesis: ex f being Function of NAT ,F₂() st
( f = g . d & f9 . n = f . n )
take f9 ; :: thesis: ( f9 = g . d & f9 . n = f9 . n )
thus ( f9 = g . d & f9 . n = f9 . n ) by A43; :: thesis: verum

end;

then consider z being Element of F₂() such that
A44: ex f being Function of NAT ,F₂() st
( f = g . d & z = f . n ) ;
[x,z] in h by A42, A44;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set st x in dom h holds
x in [:F₁(),NAT :] ;
then dom h = [:F₁(),NAT :] by A39, TARSKI:2;
then reconsider h = h as Function of [:F₁(),NAT :],F₂() by A29, FUNCT_1:def 1, FUNCT_2:def 1;
take h ; :: thesis: for a being Element of F₁() holds
( h . a,0 = F₃() & ( for n being Element of NAT holds h . a,(n + 1) = F₄() . (h . a,n),a ) )
for a being Element of F₁() holds
( h . a,0 = F₃() & ( for n being Element of NAT holds h . a,(n + 1) = F₄() . (h . a,n),a ) )

proof

let a be Element of F₁(); :: thesis: ( h . a,0 = F₃() & ( for n being Element of NAT holds h . a,(n + 1) = F₄() . (h . a,n),a ) )
consider f9 being Function of NAT ,F₂() such that
A45: g . a = f9 and
A46: f9 . 0 = F₃() and
A47: for n being Element of NAT holds f9 . (n + 1) = F₄() . (f9 . n),a by A28;

A48: now

let k be Element of NAT ; :: thesis: h . a,(k + 1) = F₄() . (h . a,k),a
[a,(k + 1)] in [:F₁(),NAT :] by ZFMISC_1:def 2;
then [a,(k + 1)] in dom h by FUNCT_2:def 1;
then consider u being set such that
A49: [[a,(k + 1)],u] in h by RELAT_1:def 4;
[a,k] in [:F₁(),NAT :] by ZFMISC_1:def 2;
then [a,k] in dom h by FUNCT_2:def 1;
then consider v being set such that
A50: [[a,k],v] in h by RELAT_1:def 4;
consider n1 being Element of NAT , d1 being Element of F₁(), z1 being Element of F₂() such that
A51: [[a,k],v] = [[d1,n1],z1] and
A52: ex f2 being Function of NAT ,F₂() st
( f2 = g . d1 & z1 = f2 . n1 ) by A50;
A53: v = [[d1,n1],z1] `2 by A51, MCART_1:def 2
.= z1 by MCART_1:def 2 ;
A54: [a,k] = [[d1,n1],z1] `1 by A51, MCART_1:def 1
.= [d1,n1] by MCART_1:def 1 ;
then A55: n1 = [a,k] `2 by MCART_1:def 2
.= k by MCART_1:def 2 ;
consider f2 being Function of NAT ,F<sub>2</sub>() such that
A56: f2 = g . d1 and
A57: z1 = f2 . n1 by A52;
consider n being Element of NAT , d being Element of F<sub>1</sub>(), z being Element of F<sub>2</sub>() such that
A58: [[a,(k + 1)],u] = [[d,n],z] and
A59: ex f1 being Function of NAT ,F<sub>2</sub>() st
( f1 = g . d & z = f1 . n ) by A49;
A60: [a,(k + 1)] = [[d,n],z] `1 by A58, MCART_1:def 1
.= [d,n] by MCART_1:def 1 ;
then A61: n = [a,(k + 1)] `2 by MCART_1:def 2
.= k + 1 by MCART_1:def 2 ;
A62: d1 = [a,k] `1 by A54, MCART_1:def 1
.= a by MCART_1:def 1 ;
A63: d = [a,(k + 1)] `1 by A60, MCART_1:def 1
.= a by MCART_1:def 1 ;
u = [[d,n],z] `2 by A58, MCART_1:def 2
.= z by MCART_1:def 2 ;
hence h . a,(k + 1) = f9 . n by A45, A49, A59, A63, FUNCT_1:8
.= F₄() . (f2 . n1),a by A45, A47, A61, A56, A55, A62
.= F₄() . (h . a,k),a by A50, A57, A53, FUNCT_1:8 ;
:: thesis: verum

end;

[a,0 ] in [:F₁(),NAT :] by ZFMISC_1:def 2;
then [a,0 ] in dom h by FUNCT_2:def 1;
then consider u being set such that
A64: [[a,0 ],u] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of F₁(), z being Element of F₂() such that
A65: [[a,0 ],u] = [[d,n],z] and
A66: ex f1 being Function of NAT ,F₂() st
( f1 = g . d & z = f1 . n ) by A64;
A67: u = [[d,n],z] `2 by A65, MCART_1:def 2
.= z by MCART_1:def 2 ;
A68: [a,0 ] = [[d,n],z] `1 by A65, MCART_1:def 1
.= [d,n] by MCART_1:def 1 ;
then A69: d = [a,0 ] `1 by MCART_1:def 1
.= a by MCART_1:def 1 ;
n = [a,0 ] `2 by A68, MCART_1:def 2
.= 0 by MCART_1:def 2 ;
hence ( h . a,0 = F₃() & ( for n being Element of NAT holds h . a,(n + 1) = F₄() . (h . a,n),a ) ) by A45, A46, A64, A66, A67, A69, A48, FUNCT_1:8; :: thesis: verum

end;

hence for a being Element of F₁() holds
( h . a,0 = F₃() & ( for n being Element of NAT holds h . a,(n + 1) = F₄() . (h . a,n),a ) ) ; :: thesis: verum