A3:
for n being Nat

for x being set ex y being set st P_{1}[n,x,y]
by A1;

consider f being Function such that

A4: ( dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 1(A3);

A5: for n being Nat

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

y1 = y2 by A2;

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 P_{1}[n,f . n,f . (n + 1)] ) )
:: 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 P_{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 P_{1}[n,f . n,f . (n + 1)] ) ) holds

y1 = y2

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{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 P_{1}[n,f . n,f . (n + 1)] ) ) implies y1 = y2 )

given f1 being Function such that A6: y1 = f1 . F_{2}()
and

A7: dom f1 = NAT and

A8: f1 . 0 = F_{1}()
and

A9: for n being Nat holds P_{1}[n,f1 . n,f1 . (n + 1)]
; :: 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 P_{1}[n,f . n,f . (n + 1)] ) or y1 = y2 )

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

given f2 being Function such that A11: y2 = f2 . F_{2}()
and

A12: dom f2 = NAT and

A13: f2 . 0 = F_{1}()
and

A14: for n being Nat holds P_{1}[n,f2 . n,f2 . (n + 1)]
; :: thesis: y1 = y2

A15: for n being Nat holds P_{1}[n,f2 . n,f2 . (n + 1)]
by A14;

f1 = f2 from NAT_1:sch 13(A7, A8, A10, A12, A13, A15, A5);

hence y1 = y2 by A6, A11; :: thesis: verum

for x being set ex y being set st P

consider f being Function such that

A4: ( dom f = NAT & f . 0 = F

A5: for n being Nat

for x, y1, y2 being set st P

y1 = y2 by A2;

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
f . F_{2}()
; :: thesis: ex f being Function st

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

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

thus ( f . F_{2}() = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) )
by A4; :: thesis: verum

end;( f . F

take f ; :: thesis: ( f . F

thus ( f . F

( y1 = f . F

( y2 = f . F

given f1 being Function such that A6: y1 = f1 . F

A7: dom f1 = NAT and

A8: f1 . 0 = F

A9: for n being Nat holds P

( not y2 = f . F

A10: for n being Nat holds P

given f2 being Function such that A11: y2 = f2 . F

A12: dom f2 = NAT and

A13: f2 . 0 = F

A14: for n being Nat holds P

A15: for n being Nat holds P

f1 = f2 from NAT_1:sch 13(A7, A8, A10, A12, A13, A15, A5);

hence y1 = y2 by A6, A11; :: thesis: verum