defpred S_{1}[ set , set , set ] means ( P_{1}[$1,$2 `1 ,$2 `2 ,$3 `2 ] & $2 `2 = $3 `1 );

A2: for n being Nat

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

A4: ( g . 0 = [F_{2}(),F_{3}()] & ( for n being Nat holds S_{1}[n,g . n,g . (n + 1)] ) )
from RECDEF_1:sch 2(A2);

deffunc H_{1}( Nat) -> Element of F_{1}() = (g . $1) `1 ;

A5: for x being Element of NAT holds H_{1}(x) in F_{1}()
;

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

A6: for x being Element of NAT holds f . x = H_{1}(x)
from FUNCT_2:sch 8(A5);

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

A10: S_{1}[ 0 ,g . 0,g . (0 + 1)]
by A4;

A11: f . 0 = (g . 0) `1 by A6

.= F_{2}()
by A4
;

f . 1 = (g . 1) `1 by A6

.= F_{3}()
by A4, A10
;

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

A2: for n being Nat

for x being Element of [:F

proof

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

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

set z = x `1 ;

set w = x `2 ;

reconsider z = x `1 , w = x `2 as Element of F_{1}() ;

consider s being Element of F_{1}() such that

A3: P_{1}[n,z,w,s]
by A1;

set y = [w,s];

reconsider y = [w,s] as Element of [:F_{1}(),F_{1}():] ;

take y ; :: thesis: S_{1}[n,x,y]

thus S_{1}[n,x,y]
by A3; :: thesis: verum

end;let x be Element of [:F

set z = x `1 ;

set w = x `2 ;

reconsider z = x `1 , w = x `2 as Element of F

consider s being Element of F

A3: P

set y = [w,s];

reconsider y = [w,s] as Element of [:F

take y ; :: thesis: S

thus S

A4: ( g . 0 = [F

deffunc H

A5: for x being Element of NAT holds H

consider f being sequence of F

A6: for x being Element of NAT holds f . x = H

A7: now :: thesis: for n being Nat holds P_{1}[n,f . n,f . (n + 1),f . (n + 2)]

take
f
; :: thesis: ( f . 0 = Flet n be Nat; :: thesis: P_{1}[n,f . n,f . (n + 1),f . (n + 2)]

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

A8: f . n = (g . nn) `1 by A6;

S_{1}[n + 1,g . (n + 1),g . ((n + 1) + 1)]
by A4;

then A9: f . (n + 2) = (g . (n + 1)) `2 by A6;

f . (n + 1) = (g . (n + 1)) `1 by A6

.= (g . nn) `2 by A4 ;

hence P_{1}[n,f . n,f . (n + 1),f . (n + 2)]
by A4, A8, A9; :: thesis: verum

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

A8: f . n = (g . nn) `1 by A6;

S

then A9: f . (n + 2) = (g . (n + 1)) `2 by A6;

f . (n + 1) = (g . (n + 1)) `1 by A6

.= (g . nn) `2 by A4 ;

hence P

A10: S

A11: f . 0 = (g . 0) `1 by A6

.= F

f . 1 = (g . 1) `1 by A6

.= F

hence ( f . 0 = F