defpred S1[ object , object , object , object , object ] means P1[\$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 [:F1(),F2():]
for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
proof
let n be Nat; :: thesis: for x being Element of [:F1(),F2():]
for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]

let x be Element of [:F1(),F2():]; :: thesis: for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
let y be Element of [:F3(),F4():]; :: thesis: ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
( x `1 is Element of F1() & x `2 is Element of F2() & y `1 is Element of F3() & y `2 is Element of F4() ) by MCART_1:10;
then consider ai being Element of F1(), bi being Element of F2(), ci being Element of F3(), di being Element of F4() such that
A3: P1[n,x `1 ,x `2 ,y `1 ,y `2 ,ai,bi,ci,di] by A1;
reconsider z = [ai,bi] as Element of [:F1(),F2():] by ZFMISC_1:87;
reconsider w = [ci,di] as Element of [:F3(),F4():] by ZFMISC_1:87;
take z ; :: thesis: ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
take w ; :: thesis: S1[n,x,y,z,w]
thus S1[n,x,y,z,w] by A3; :: thesis: verum
end;
reconsider AB0 = [F5(),F6()] as Element of [:F1(),F2():] by ZFMISC_1:87;
reconsider CD0 = [F7(),F8()] as Element of [:F3(),F4():] by ZFMISC_1:87;
consider fg being sequence of [:F1(),F2():], hi being sequence of [:F3(),F4():] such that
A4: fg . 0 = AB0 and
A5: hi . 0 = CD0 and
A6: for e being Nat holds S1[e,fg . e,hi . e,fg . (e + 1),hi . (e + 1)] from take pr1 fg ; :: thesis: ex g being sequence of F2() ex h being sequence of F3() ex i being sequence of F4() st
( (pr1 fg) . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Nat holds P1[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 F3() ex i being sequence of F4() st
( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Nat holds P1[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 F4() st
( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & i . 0 = F8() & ( for n being Nat holds P1[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 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() & ( for n being Nat holds P1[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 ;
hence ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() ) by A4, A5; :: thesis: for n being Nat holds P1[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 Nat; :: thesis: P1[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 ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
( (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 ;
hence P1[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