defpred S₁[ set , set , set ] means P₁[$1,$2 `1 ,$2 `2 ,$3 `1 ,$3 `2 ];
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]
consider ai being Element of F₁(), bi being Element of F₂() such that
A3: P₁[n,x `1 ,x `2 ,ai,bi] by A1;
take [ai,bi] ; :: thesis: S₁[n,x,[ai,bi]]
thus S₁[n,x,[ai,bi]] by A3; :: thesis: verum

end;

consider f being sequence of [:F₁(),F₂():] such that
A4: f . 0 = [F₃(),F₄()] and
A5: for e being Nat holds S₁[e,f . e,f . (e + 1)] from RECDEF_1:sch 2(A2);
take pr1 f ; :: thesis: ex g being sequence of F₂() st
( (pr1 f) . 0 = F₃() & g . 0 = F₄() & ( for n being Nat holds P₁[n,(pr1 f) . n,g . n,(pr1 f) . (n + 1),g . (n + 1)] ) )
take pr2 f ; :: thesis: ( (pr1 f) . 0 = F₃() & (pr2 f) . 0 = F₄() & ( for n being Nat holds P₁[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)] ) )
( [F₃(),F₄()] `1 = F<sub>3</sub>() & [F<sub>3</sub>(),F<sub>4</sub>()] `2 = F₄() ) ;
hence ( (pr1 f) . 0 = F₃() & (pr2 f) . 0 = F₄() ) by A4, FUNCT_2:def 5, FUNCT_2:def 6; :: thesis: for n being Nat holds P₁[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)]
let i be Nat; :: thesis: P₁[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
A6: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def 5, FUNCT_2:def 6;
i in NAT by ORDINAL1:def 12;
then ( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 5, FUNCT_2:def 6;
hence P₁[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A5, A6; :: thesis: verum