defpred S_{1}[ set , set , set ] means for z being set st z = $2 holds

$3 = F_{3}($1,z);

A1: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

for x, y1, y2 being set st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2

( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) ) & ex f being Function st

( y2 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) ) holds

y1 = y2 ) ) from RECDEF_1:sch 11(A1, A2);

then consider y being set , f being Function such that

A6: ( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
;

thus ex y being set ex f being Function st

( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) )
:: thesis: for y1, y2 being set st ex f being Function st

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) & ex f being Function st

( y2 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) holds

y1 = y2

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) & ex f being Function st

( y2 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) implies y1 = y2 )

given f1 being Function such that A7: ( y1 = f1 . F_{2}() & dom f1 = NAT & f1 . 0 = F_{1}() )
and

A8: for n being Nat holds f1 . (n + 1) = F_{3}(n,(f1 . n))
; :: thesis: ( for f being Function holds

( not y2 = f . F_{2}() or not dom f = NAT or not f . 0 = F_{1}() or ex n being Nat st not f . (n + 1) = F_{3}(n,(f . n)) ) or y1 = y2 )

A9: for n being Nat holds S_{1}[n,f1 . n,f1 . (n + 1)]
by A8;

given f2 being Function such that A10: ( y2 = f2 . F_{2}() & dom f2 = NAT & f2 . 0 = F_{1}() )
and

A11: for n being Nat holds f2 . (n + 1) = F_{3}(n,(f2 . n))
; :: thesis: y1 = y2

for n being Nat holds S_{1}[n,f2 . n,f2 . (n + 1)]
by A11;

hence y1 = y2 by A5, A7, A10, A9; :: thesis: verum

$3 = F

A1: for n being Nat

for x being set ex y being set st S

proof

A2:
for n being Nat
let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

take F_{3}(n,x)
; :: thesis: S_{1}[n,x,F_{3}(n,x)]

thus S_{1}[n,x,F_{3}(n,x)]
; :: thesis: verum

end;let x be set ; :: thesis: ex y being set st S

take F

thus S

for x, y1, y2 being set st S

y1 = y2

proof

A5:
( ex y being set ex f being Function st
let n be Nat; :: thesis: for x, y1, y2 being set st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2

let x, y1, y2 be set ; :: thesis: ( S_{1}[n,x,y1] & S_{1}[n,x,y2] implies y1 = y2 )

assume that

A3: for z being set st z = x holds

y1 = F_{3}(n,z)
and

A4: for z being set st z = x holds

y2 = F_{3}(n,z)
; :: thesis: y1 = y2

thus y1 = F_{3}(n,x)
by A3

.= y2 by A4 ; :: thesis: verum

end;y1 = y2

let x, y1, y2 be set ; :: thesis: ( S

assume that

A3: for z being set st z = x holds

y1 = F

A4: for z being set st z = x holds

y2 = F

thus y1 = F

.= y2 by A4 ; :: thesis: verum

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) ) from RECDEF_1:sch 11(A1, A2);

then consider y being set , f being Function such that

A6: ( y = f . F

thus ex y being set ex f being Function st

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2

proof

let y1, y2 be set ; :: thesis: ( ex f being Function st
take
y
; :: thesis: ex f being Function st

( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) )

take f ; :: thesis: ( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) )

thus ( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) )
by A6; :: thesis: verum

end;( y = f . F

take f ; :: thesis: ( y = f . F

thus ( y = f . F

( y1 = f . F

( y2 = f . F

given f1 being Function such that A7: ( y1 = f1 . F

A8: for n being Nat holds f1 . (n + 1) = F

( not y2 = f . F

A9: for n being Nat holds S

given f2 being Function such that A10: ( y2 = f2 . F

A11: for n being Nat holds f2 . (n + 1) = F

for n being Nat holds S

hence y1 = y2 by A5, A7, A10, A9; :: thesis: verum