A3:
for n being 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 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
by A2;
thus
ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being 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 Nat holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2proof
take
f . F2()
;
ex f being Function st
( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
take
f
;
( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus
(
f . F2()
= f . F2() &
dom f = NAT &
f . 0 = F1() & ( for
n being
Nat holds
P1[
n,
f . n,
f . (n + 1)] ) )
by A4;
verum
end;
let y1, y2 be set ; ( ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being 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 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 Nat holds P1[n,f1 . n,f1 . (n + 1)]
; ( for f being Function holds
( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being 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)]
by A9;
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 Nat holds P1[n,f2 . n,f2 . (n + 1)]
; y1 = y2
A15:
for n being Nat holds P1[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; verum