defpred S₁[ set , set , set , set , set ] means P₁[$1,$2 `1 ,$2 `2 ,$3 `1 ,$3 `2 ,$4 `1 ,$4 `2 ,$5 `1 ,$5 `2 ];
A2: for n being Nat
for x being Element of [:F₁(),F₂():]
for y being Element of [:F₃(),F₄():] ex z being Element of [:F₁(),F₂():] ex w being Element of [:F₃(),F₄():] st S₁[n,x,y,z,w]

proof

let n be Nat; :: thesis: for x being Element of [:F₁(),F₂():]
for y being Element of [:F₃(),F₄():] ex z being Element of [:F₁(),F₂():] ex w being Element of [:F₃(),F₄():] st S₁[n,x,y,z,w]
let x be Element of [:F₁(),F₂():]; :: thesis: for y being Element of [:F₃(),F₄():] ex z being Element of [:F₁(),F₂():] ex w being Element of [:F₃(),F₄():] st S₁[n,x,y,z,w]
let y be Element of [:F₃(),F₄():]; :: thesis: ex z being Element of [:F₁(),F₂():] ex w being Element of [:F₃(),F₄():] st S₁[n,x,y,z,w]
n in NAT by ORDINAL1:def 12;
then consider ai being Element of F₁(), bi being Element of F₂(), ci being Element of F₃(), di being Element of F₄() such that
A3: P₁[n,x `1 ,x `2 ,y `1 ,y `2 ,ai,bi,ci,di] by A1;
take z = [ai,bi]; :: thesis: ex w being Element of [:F₃(),F₄():] st S₁[n,x,y,z,w]
take w = [ci,di]; :: thesis: S₁[n,x,y,z,w]
thus S₁[n,x,y,z,w] by A3; :: thesis: verum

end;

set AB0 = [F₅(),F₆()];
set CD0 = [F₇(),F₈()];
consider fg being sequence of [:F₁(),F₂():], hi being sequence of [:F₃(),F₄():] such that
A4: fg . 0 = [F₅(),F₆()] and
A5: hi . 0 = [F₇(),F₈()] and
A6: for e being Nat holds S₁[e,fg . e,hi . e,fg . (e + 1),hi . (e + 1)] from RECDEF_2:sch 3(A2);
take pr1 fg ; :: thesis: ex g being sequence of F₂() ex h being sequence of F₃() ex i being sequence of F₄() st
( (pr1 fg) . 0 = F₅() & g . 0 = F₆() & h . 0 = F₇() & i . 0 = F₈() & ( for n being Element of NAT holds P₁[n,(pr1 fg) . n,g . n,h . n,i . n,(pr1 fg) . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )
take pr2 fg ; :: thesis: ex h being sequence of F₃() ex i being sequence of F₄() st
( (pr1 fg) . 0 = F₅() & (pr2 fg) . 0 = F₆() & h . 0 = F₇() & i . 0 = F₈() & ( for n being Element of NAT holds P₁[n,(pr1 fg) . n,(pr2 fg) . n,h . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),h . (n + 1),i . (n + 1)] ) )
take pr1 hi ; :: thesis: ex i being sequence of F₄() st
( (pr1 fg) . 0 = F₅() & (pr2 fg) . 0 = F₆() & (pr1 hi) . 0 = F₇() & i . 0 = F₈() & ( for n being Element of NAT holds P₁[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),i . (n + 1)] ) )
take pr2 hi ; :: thesis: ( (pr1 fg) . 0 = F₅() & (pr2 fg) . 0 = F₆() & (pr1 hi) . 0 = F₇() & (pr2 hi) . 0 = F₈() & ( for n being Element of NAT holds P₁[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)] ) )
( (fg . 0) `1 = (pr1 fg) . 0 & (fg . 0) `2 = (pr2 fg) . 0 & (hi . 0) `1 = (pr1 hi) . 0 & (hi . 0) `2 = (pr2 hi) . 0 ) by FUNCT_2:def 5, FUNCT_2:def 6;
hence ( (pr1 fg) . 0 = F₅() & (pr2 fg) . 0 = F₆() & (pr1 hi) . 0 = F₇() & (pr2 hi) . 0 = F₈() ) by A4, A5; :: thesis: for n being Element of NAT holds P₁[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)]
let i be Element of NAT ; :: thesis: P₁[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)]
A7: ( (fg . (i + 1)) `1 = (pr1 fg) . (i + 1) & (fg . (i + 1)) `2 = (pr2 fg) . (i + 1) & (hi . (i + 1)) `1 = (pr1 hi) . (i + 1) & (hi . (i + 1)) `2 = (pr2 hi) . (i + 1) ) by FUNCT_2:def 5, FUNCT_2:def 6;
( (fg . i) `1 = (pr1 fg) . i & (fg . i) `2 = (pr2 fg) . i & (hi . i) `1 = (pr1 hi) . i & (hi . i) `2 = (pr2 hi) . i ) by FUNCT_2:def 5, FUNCT_2:def 6;
hence P₁[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)] by A6, A7; :: thesis: verum