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

proof

let n be Element of 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]]
[ai,bi] `1 = ai by MCART_1:7;
hence S₁[n,x,[ai,bi]] by A3, MCART_1:7; :: thesis: verum

end;

consider f being Function of NAT,[:F₁(),F₂():] such that
A4: f . 0 = [F₃(),F₄()] and
A5: for e being Element of NAT holds S₁[e,f . e,f . (e + 1)] from RECDEF_1:sch 2(A2);
take pr1 f ; :: thesis: ex g being Function of NAT,F₂() st
( (pr1 f) . 0 = F₃() & g . 0 = F₄() & ( for n being Element of 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 Element of NAT holds P₁[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)] ) )
( (f . 0) `1 = (pr1 f) . 0 & (f . 0) `2 = (pr2 f) . 0 ) by FUNCT_2:def 6, FUNCT_2:def 7;
hence ( (pr1 f) . 0 = F₃() & (pr2 f) . 0 = F₄() ) by A4, MCART_1:def 1, MCART_1:def 2; :: thesis: for n being Element of NAT holds P₁[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)]
let i be Element of 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 6, FUNCT_2:def 7;
( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 6, FUNCT_2:def 7;
hence P₁[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A5, A6; :: thesis: verum