A3: for n being Element of NAT
for x being set ex y being set st P1[n,x,y] by A1;
consider f being Function such that
A4: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A3);
 A5: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
let n be Nat; :: thesis: for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
n in NAT by ORDINAL1:def 13;
hence for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 by A2; :: thesis: verum
end;
thus ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) :: thesis: for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2
proof
take f . F2() ; :: thesis: ex f being Function st
( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
take f ; :: thesis: ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
thus ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) by A4; :: thesis: verum
end;
let y1, y2 be set ; :: thesis: ( ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) implies y1 = y2 )
given f1 being Function such that A6: y1 = f1 . F2() and
A7: dom f1 = NAT and
A8: f1 . 0 = F1() and
A9: for n being Element of NAT holds P1[n,f1 . n,f1 . (n + 1)] ; :: thesis: ( for f being Function holds
( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being Element of NAT st P1[n,f . n,f . (n + 1)] ) or y1 = y2 )
A10: for n being Nat holds P1[n,f1 . n,f1 . (n + 1)]
proof
let n be Nat; :: thesis: P1[n,f1 . n,f1 . (n + 1)]
n in NAT by ORDINAL1:def 13;
hence P1[n,f1 . n,f1 . (n + 1)] by A9; :: thesis: verum
end;
given f2 being Function such that A11: y2 = f2 . F2() and
A12: dom f2 = NAT and
A13: f2 . 0 = F1() and
A14: for n being Element of NAT holds P1[n,f2 . n,f2 . (n + 1)] ; :: thesis: y1 = y2
A15: for n being Nat holds P1[n,f2 . n,f2 . (n + 1)]
proof
let n be Nat; :: thesis: P1[n,f2 . n,f2 . (n + 1)]
n in NAT by ORDINAL1:def 13;
hence P1[n,f2 . n,f2 . (n + 1)] by A14; :: thesis: verum
end;
f1 = f2 from NAT_1:sch 13(A7, A8, A10, A12, A13, A15, A5);
 hence y1 = y2 by A6, A11; :: thesis: verum