defpred S₁[ set , set , set ] means ( P₁[$1,$2 `1 ,$2 `2 ,$3 `2 ] & $2 `2 = $3 `1 );
A2: for n being Nat
for x being Element of [:F₁(),F₁():] ex y being Element of [:F₁(),F₁():] st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of [:F₁(),F₁():] ex y being Element of [:F₁(),F₁():] st S₁[n,x,y]
let x be Element of [:F₁(),F₁():]; :: thesis: ex y being Element of [:F₁(),F₁():] st S₁[n,x,y]
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₁() such that
A3: P₁[n,z,w,s] by A1;
set y = [w,s];
reconsider y = [w,s] as Element of [:F₁(),F₁():] ;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A3; :: thesis: verum

end;

consider g being sequence of [:F₁(),F₁():] such that
A4: ( g . 0 = [F₂(),F₃()] & ( for n being Nat holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
deffunc H₁( Nat) -> Element of F₁() = (g . $1) `1 ;
A5: for x being Element of NAT holds H₁(x) in F₁() ;
consider f being sequence of F₁() such that
A6: for x being Element of NAT holds f . x = H₁(x) from FUNCT_2:sch 8(A5);

A7: now :: thesis: for n being Nat holds P₁[n,f . n,f . (n + 1),f . (n + 2)]

let n be Nat; :: thesis: P₁[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<sub>1</sub>[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₁[n,f . n,f . (n + 1),f . (n + 2)] by A4, A8, A9; :: thesis: verum

end;

take f ; :: thesis: ( f . 0 = F₂() & f . 1 = F₃() & ( for n being Nat holds P₁[n,f . n,f . (n + 1),f . (n + 2)] ) )
A10: S₁[ 0 ,g . 0,g . (0 + 1)] by A4;
A11: f . 0 = (g . 0) `1 by A6
.= F<sub>2</sub>() by A4 ;
f . 1 = (g . 1) `1 by A6
.= F₃() by A4, A10 ;
hence ( f . 0 = F₂() & f . 1 = F₃() & ( for n being Nat holds P₁[n,f . n,f . (n + 1),f . (n + 2)] ) ) by A11, A7; :: thesis: verum