defpred S_{1}[ set , set , set ] means for z being Element of F_{1}() st z = $2 holds

$3 = F_{4}($1,z);

A1: for n being Nat

for x being Element of F_{1}() ex y being Element of F_{1}() st S_{1}[n,x,y]

for x, y1, y2 being Element of F_{1}() st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

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

( y = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) ) & ( 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 S_{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 S_{1}[n,f . n,f . (n + 1)] ) ) holds

y1 = y2 ) ) from RECDEF_1:sch 13(A1, A2);

then consider y being Element of F_{1}(), f being sequence of F_{1}() such that

A6: ( y = f . F_{3}() & f . 0 = F_{2}() )
and

A7: for n being Nat holds S_{1}[n,f . n,f . (n + 1)]
;

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 f . (n + 1) = F_{4}(n,(f . n)) ) )
:: 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 f . (n + 1) = F_{4}(n,(f . n)) ) ) & ex f being sequence of F_{1}() st

( y2 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = F_{4}(n,(f . n)) ) ) 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 f . (n + 1) = F_{4}(n,(f . n)) ) ) & ex f being sequence of F_{1}() st

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

given f being sequence of F_{1}() such that A8:
( y1 = f . F_{3}() & f . 0 = F_{2}() )
and

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

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

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

A12: for n being Nat holds f2 . (n + 1) = F_{4}(n,(f2 . n))
; :: thesis: y1 = y2

for n being Nat holds S_{1}[n,f2 . n,f2 . (n + 1)]
by A12;

hence y1 = y2 by A5, A8, A11, A10; :: thesis: verum

$3 = F

A1: for n being Nat

for x being Element of F

proof

A2:
for n being Nat
let n be Nat; :: thesis: for x being Element of F_{1}() ex y being Element of F_{1}() st S_{1}[n,x,y]

let x be Element of F_{1}(); :: thesis: ex y being Element of F_{1}() st S_{1}[n,x,y]

take F_{4}(n,x)
; :: thesis: S_{1}[n,x,F_{4}(n,x)]

let z be Element of F_{1}(); :: thesis: ( z = x implies F_{4}(n,x) = F_{4}(n,z) )

assume z = x ; :: thesis: F_{4}(n,x) = F_{4}(n,z)

hence F_{4}(n,x) = F_{4}(n,z)
; :: thesis: verum

end;let x be Element of F

take F

let z be Element of F

assume z = x ; :: thesis: F

hence F

for x, y1, y2 being Element of F

y1 = y2

proof

A5:
( ex y being Element of F
let n be Nat; :: thesis: for x, y1, y2 being Element of F_{1}() st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2

let x, y1, y2 be Element of F_{1}(); :: thesis: ( S_{1}[n,x,y1] & S_{1}[n,x,y2] implies y1 = y2 )

assume that

A3: for z being Element of F_{1}() st z = x holds

y1 = F_{4}(n,z)
and

A4: for z being Element of F_{1}() st z = x holds

y2 = F_{4}(n,z)
; :: thesis: y1 = y2

thus y1 = F_{4}(n,x)
by A3

.= y2 by A4 ; :: thesis: verum

end;y1 = y2

let x, y1, y2 be Element of F

assume that

A3: for z being Element of F

y1 = F

A4: for z being Element of F

y2 = F

thus y1 = F

.= y2 by A4 ; :: thesis: verum

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) ) from RECDEF_1:sch 13(A1, A2);

then consider y being Element of F

A6: ( y = f . F

A7: for n being Nat holds S

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
take
y
; :: thesis: ex f being sequence of F_{1}() st

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

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

thus ( y = f . F_{3}() & f . 0 = F_{2}() )
by A6; :: thesis: for n being Nat holds f . (n + 1) = F_{4}(n,(f . n))

let n be Nat; :: thesis: f . (n + 1) = F_{4}(n,(f . n))

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S_{1}[n,f . n,f . (n + 1)]
by A7;

hence f . (n + 1) = F_{4}(n,(f . n))
; :: thesis: verum

end;( y = f . F

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

thus ( y = f . F

let n be Nat; :: thesis: f . (n + 1) = F

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S

hence f . (n + 1) = F

( y1 = f . F

( y2 = f . F

given f being sequence of F

A9: for n being Nat holds f . (n + 1) = F

( not y2 = f . F

A10: for n being Nat holds S

given f2 being sequence of F

A12: for n being Nat holds f2 . (n + 1) = F

for n being Nat holds S

hence y1 = y2 by A5, A8, A11, A10; :: thesis: verum