A1: for a being Element of F1() ex f being Function of NAT ,F2() st
( f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
proof
let a be Element of F1(); :: thesis: ex f being Function of NAT ,F2() st
( f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
defpred S1[ Element of NAT , Element of F2(), Element of F2()] means $3 = F4() . a,$2;
A2: for n being Element of NAT
for x being Element of F2() ex y being Element of F2() st S1[n,x,y] ;
ex f being Function of NAT ,F2() st
( f . 0 = F3() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
 hence ex f being Function of NAT ,F2() st
( f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) ; :: 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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
proof
set h = { [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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) } ;
A3: now
let x, y1, y2 be set ; :: 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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . 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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) } implies y1 = y2 )
assume that
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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) } and
A5: [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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) } ; :: thesis: y1 = y2
consider a1 being Element of F1(), l1 being Element of Funcs NAT ,F2() such that
A6: [x,y1] = [a1,l1] and
A7: ex f being Function of NAT ,F2() st
( f = l1 & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a1,(f . n) ) ) by A4;
consider a2 being Element of F1(), l2 being Element of Funcs NAT ,F2() such that
A8: [x,y2] = [a2,l2] and
A9: ex f being Function of NAT ,F2() st
( f = l2 & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a2,(f . n) ) ) by A5;
consider f1 being Function of NAT ,F2() such that
A10: f1 = l1 and
A11: f1 . 0 = F3() and
A12: for n being Element of NAT holds f1 . (n + 1) = F4() . a1,(f1 . n) by A7;
consider f2 being Function of NAT ,F2() such that
A13: f2 = l2 and
A14: f2 . 0 = F3() and
A15: for n being Element of NAT holds f2 . (n + 1) = F4() . a2,(f2 . n) 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 S1[ 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: ( S1[n] implies S1[n + 1] )
assume A19: S1[n] ; :: thesis: S1[n + 1]
f1 . (n + 1) = F4() . a2,(f1 . n) by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S1[n + 1] ; :: thesis: verum
end;
A20: S1[ 0 ] by A11, A14;
for n being Element of NAT holds S1[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 F1(), l is Element of Funcs NAT ,F2() : ex f being Function of NAT ,F2() st
( f = l & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . 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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . 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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) ) ;
hence x in [:F1(),(Funcs NAT ,F2()):] by ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider h = { [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() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) } as Relation of F1(),(Funcs NAT ,F2()) by TARSKI:def 3;
A22: for x being set st x in F1() holds
x in dom h
proof
let x be set ; :: thesis: ( x in F1() implies x in dom h )
assume A23: x in F1() ; :: thesis: x in dom h
then consider f being Function of NAT ,F2() such that
A24: ( f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . x,(f . n) ) ) by A1;
reconsider f9 = f as Element of Funcs NAT ,F2() 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 F1() ;
then dom h = F1() by A22, TARSKI:2;
then reconsider h = h as Function of F1(),(Funcs NAT ,F2()) by A3, FUNCT_1:def 1, FUNCT_2:def 1;
take h ; :: thesis: for a being Element of F1() ex f being Function of NAT ,F2() st
( h . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
for a being Element of F1() ex f being Function of NAT ,F2() st
( h . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
proof
let a be Element of F1(); :: thesis: ex f being Function of NAT ,F2() st
( h . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) )
dom h = F1() by FUNCT_2:def 1;
then [a,(h . a)] in h by FUNCT_1:8;
then consider a9 being Element of F1(), l being Element of Funcs NAT ,F2() such that
A25: [a,(h . a)] = [a9,l] and
A26: ex f9 being Function of NAT ,F2() st
( f9 = l & f9 . 0 = F3() & ( for n being Element of NAT holds f9 . (n + 1) = F4() . a9,(f9 . n) ) ) ;
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 ,F2() st
( h . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) by A26, A27; :: thesis: verum
end;
hence for a being Element of F1() ex f being Function of NAT ,F2() st
( h . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) ; :: thesis: verum
end;
then consider g being Function of F1(),(Funcs NAT ,F2()) such that
A28: for a being Element of F1() ex f being Function of NAT ,F2() st
( g . a = f & f . 0 = F3() & ( for n being Element of NAT holds f . (n + 1) = F4() . a,(f . n) ) ) ;
set h = { [[n,a],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 ) } ;
A29: now
let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [[n,a],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 { [[n,a],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 that
A30: [x,y1] in { [[n,a],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 ) } and
A31: [x,y2] in { [[n,a],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
consider n1 being Element of NAT , a1 being Element of F1(), z1 being Element of F2() such that
A32: [x,y1] = [[n1,a1],z1] and
A33: ex f1 being Function of NAT ,F2() st
( f1 = g . a1 & z1 = f1 . n1 ) by A30;
consider n2 being Element of NAT , a2 being Element of F1(), z2 being Element of F2() such that
A34: [x,y2] = [[n2,a2],z2] and
A35: ex f2 being Function of NAT ,F2() st
( f2 = g . a2 & z2 = f2 . n2 ) by A31;
A36: [n1,a1] = [x,y1] `1 by A32, MCART_1:def 1
.= x by MCART_1:def 1
.= [[n2,a2],z2] `1 by A34, MCART_1:def 1
.= [n2,a2] by MCART_1:def 1 ;
then A37: a1 = [n2,a2] `2 by MCART_1:def 2
.= a2 by MCART_1:def 2 ;
n1 = [n2,a2] `1 by A36, MCART_1:def 1
.= n2 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 { [[n,a],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 [:[:NAT ,F1():],F2():] )
assume x in { [[n,a],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 [:[:NAT ,F1():],F2():]
then consider n1 being Element of NAT , a1 being Element of F1(), z1 being Element of F2() such that
A38: x = [[n1,a1],z1] and
ex f1 being Function of NAT ,F2() st
( f1 = g . a1 & z1 = f1 . n1 ) ;
[n1,a1] in [:NAT ,F1():] by ZFMISC_1:def 2;
hence x in [:[:NAT ,F1():],F2():] by A38, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider h = { [[n,a],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 [:NAT ,F1():],F2() by TARSKI:def 3;
A39: for x being set st x in [:NAT ,F1():] holds
x in dom h
proof
let x be set ; :: thesis: ( x in [:NAT ,F1():] implies x in dom h )
assume x in [:NAT ,F1():] ; :: thesis: x in dom h
then consider n, d being set such that
A40: n in NAT and
A41: d in F1() and
A42: x = [n,d] by ZFMISC_1:def 2;
reconsider d = d as Element of F1() by A41;
reconsider n = n as Element of NAT by A40;
consider f9 being Function of NAT ,F2() such that
A43: g . d = f9 and
f9 . 0 = F3() and
for n being Element of NAT holds f9 . (n + 1) = F4() . d,(f9 . n) by A28;
ex z being Element of F2() ex f being Function of NAT ,F2() st
( f = g . d & z = f . n )
proof
take f9 . n ; :: thesis: ex f being Function of NAT ,F2() 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 F2() such that
A44: ex f being Function of NAT ,F2() 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 [:NAT ,F1():] ;
then dom h = [:NAT ,F1():] by A39, TARSKI:2;
then reconsider h = h as Function of [:NAT ,F1():],F2() by A29, FUNCT_1:def 1, FUNCT_2:def 1;
take h ; :: thesis: for a being Element of F1() holds
( h . 0 ,a = F3() & ( for n being Element of NAT holds h . (n + 1),a = F4() . a,(h . n,a) ) )
for a being Element of F1() holds
( h . 0 ,a = F3() & ( for n being Element of NAT holds h . (n + 1),a = F4() . a,(h . n,a) ) )
proof
let a be Element of F1(); :: thesis: ( h . 0 ,a = F3() & ( for n being Element of NAT holds h . (n + 1),a = F4() . a,(h . n,a) ) )
consider f9 being Function of NAT ,F2() such that
A45: g . a = f9 and
A46: f9 . 0 = F3() and
A47: for n being Element of NAT holds f9 . (n + 1) = F4() . a,(f9 . n) by A28;
A48: now
let k be Element of NAT ; :: thesis: h . (k + 1),a = F4() . a,(h . k,a)
[(k + 1),a] in [:NAT ,F1():] by ZFMISC_1:def 2;
then [(k + 1),a] in dom h by FUNCT_2:def 1;
then consider u being set such that
A49: [[(k + 1),a],u] in h by RELAT_1:def 4;
[k,a] in [:NAT ,F1():] by ZFMISC_1:def 2;
then [k,a] in dom h by FUNCT_2:def 1;
then consider v being set such that
A50: [[k,a],v] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of F1(), z being Element of F2() such that
A51: [[(k + 1),a],u] = [[n,d],z] and
A52: ex f1 being Function of NAT ,F2() st
( f1 = g . d & z = f1 . n ) by A49;
A53: u = [[n,d],z] `2 by A51, MCART_1:def 2
.= z by MCART_1:def 2 ;
consider n1 being Element of NAT , d1 being Element of F1(), z1 being Element of F2() such that
A54: [[k,a],v] = [[n1,d1],z1] and
A55: ex f2 being Function of NAT ,F2() st
( f2 = g . d1 & z1 = f2 . n1 ) by A50;
A56: v = [[n1,d1],z1] `2 by A54, MCART_1:def 2
.= z1 by MCART_1:def 2 ;
A57: [(k + 1),a] = [[n,d],z] `1 by A51, MCART_1:def 1
.= [n,d] by MCART_1:def 1 ;
then A58: d = [(k + 1),a] `2 by MCART_1:def 2
.= a by MCART_1:def 2 ;
A59: [k,a] = [[n1,d1],z1] `1 by A54, MCART_1:def 1
.= [n1,d1] by MCART_1:def 1 ;
then A60: n1 = [k,a] `1 by MCART_1:def 1
.= k by MCART_1:def 1 ;
A61: d1 = [k,a] `2 by A59, MCART_1:def 2
.= a by MCART_1:def 2 ;
n = [(k + 1),a] `1 by A57, MCART_1:def 1
.= k + 1 by MCART_1:def 1 ;
hence h . (k + 1),a = f9 . (k + 1) by A45, A49, A52, A53, A58, FUNCT_1:8
.= F4() . a,z1 by A45, A47, A55, A60, A61
.= F4() . a,(h . k,a) by A50, A56, FUNCT_1:8 ;
:: thesis: verum
end;
[0 ,a] in [:NAT ,F1():] by ZFMISC_1:def 2;
then [0 ,a] in dom h by FUNCT_2:def 1;
then consider u being set such that
A62: [[0 ,a],u] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of F1(), z being Element of F2() such that
A63: [[0 ,a],u] = [[n,d],z] and
A64: ex f1 being Function of NAT ,F2() st
( f1 = g . d & z = f1 . n ) by A62;
A65: u = [[n,d],z] `2 by A63, MCART_1:def 2
.= z by MCART_1:def 2 ;
A66: [0 ,a] = [[n,d],z] `1 by A63, MCART_1:def 1
.= [n,d] by MCART_1:def 1 ;
then A67: d = [0 ,a] `2 by MCART_1:def 2
.= a by MCART_1:def 2 ;
n = [0 ,a] `1 by A66, MCART_1:def 1
.= 0 by MCART_1:def 1 ;
hence ( h . 0 ,a = F3() & ( for n being Element of NAT holds h . (n + 1),a = F4() . a,(h . n,a) ) ) by A45, A46, A62, A64, A65, A67, A48, FUNCT_1:8; :: thesis: verum
end;
hence for a being Element of F1() holds
( h . 0 ,a = F3() & ( for n being Element of NAT holds h . (n + 1),a = F4() . a,(h . n,a) ) ) ; :: thesis: verum