A3: for n being Nat
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y] by A1;
consider f being sequence of F₁() such that
A4: ( f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A3);
A5: for n being Nat
for x, y1, y2 being Element of F₁() st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2 by A2;
thus ex y being Element of F₁() ex f being sequence of F₁() st
( y = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) :: thesis: for y1, y2 being Element of F₁() st ex f being sequence of F₁() st
( y1 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F₁() st
( y2 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) holds
y1 = y2

proof

reconsider n = F₃() as Element of NAT by ORDINAL1:def 12;
take f . n ; :: thesis: ex f being sequence of F₁() st
( f . n = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )
take f ; :: thesis: ( f . n = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )
thus ( f . n = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) by A4; :: thesis: verum

end;

let y1, y2 be Element of F₁(); :: thesis: ( ex f being sequence of F₁() st
( y1 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F₁() st
( y2 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) implies y1 = y2 )
given f1 being sequence of F₁() such that A6: y1 = f1 . F₃() and
A7: f1 . 0 = F₂() and
A8: for n being Nat holds P₁[n,f1 . n,f1 . (n + 1)] ; :: thesis: ( for f being sequence of F₁() holds
( not y2 = f . F₃() or not f . 0 = F₂() or ex n being Nat st P₁[n,f . n,f . (n + 1)] ) or y1 = y2 )
A9: f1 . 0 = F₂() by A7;
A10: for n being Nat holds P₁[n,f1 . n,f1 . (n + 1)] by A8;
given f2 being sequence of F₁() such that A11: y2 = f2 . F₃() and
A12: f2 . 0 = F₂() and
A13: for n being Nat holds P₁[n,f2 . n,f2 . (n + 1)] ; :: thesis: y1 = y2
A14: for n being Nat holds P₁[n,f2 . n,f2 . (n + 1)] by A13;
A15: f2 . 0 = F₂() by A12;
f1 = f2 from NAT_1:sch 14(A9, A10, A15, A14, A5);
hence y1 = y2 by A6, A11; :: thesis: verum