A3:
for n being Nat

for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[n,x,y]
by A1;

consider f being sequence of F_{1}() such that

A4: ( f . 0 = F_{2}() & ( for n being Nat holds P_{1}[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_{1}() st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2 by A2;

thus ex y being Element of F_{1}() ex f being sequence of F_{1}() st

( y = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) )
:: thesis: for y1, y2 being Element of F_{1}() st ex f being sequence of F_{1}() st

( y1 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F_{1}() st

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

y1 = y2_{1}(); :: thesis: ( ex f being sequence of F_{1}() st

( y1 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F_{1}() st

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

given f1 being sequence of F_{1}() such that A6:
y1 = f1 . F_{3}()
and

A7: f1 . 0 = F_{2}()
and

A8: for n being Nat holds P_{1}[n,f1 . n,f1 . (n + 1)]
; :: thesis: ( for f being sequence of F_{1}() holds

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

A9: f1 . 0 = F_{2}()
by A7;

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

given f2 being sequence of F_{1}() such that A11:
y2 = f2 . F_{3}()
and

A12: f2 . 0 = F_{2}()
and

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

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

A15: f2 . 0 = F_{2}()
by A12;

f1 = f2 from NAT_1:sch 14(A9, A10, A15, A14, A5);

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

for x being Element of F

consider f being sequence of F

A4: ( f . 0 = F

A5: for n being Nat

for x, y1, y2 being Element of F

y1 = y2 by A2;

thus ex y being Element of F

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2

proof

let y1, y2 be Element of F
reconsider n = F_{3}() as Element of NAT by ORDINAL1:def 12;

take f . n ; :: thesis: ex f being sequence of F_{1}() st

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

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

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

end;take f . n ; :: thesis: ex f being sequence of F

( f . n = f . F

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

thus ( f . n = f . F

( y1 = f . F

( y2 = f . F

given f1 being sequence of F

A7: f1 . 0 = F

A8: for n being Nat holds P

( not y2 = f . F

A9: f1 . 0 = F

A10: for n being Nat holds P

given f2 being sequence of F

A12: f2 . 0 = F

A13: for n being Nat holds P

A14: for n being Nat holds P

A15: f2 . 0 = F

f1 = f2 from NAT_1:sch 14(A9, A10, A15, A14, A5);

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