defpred S1[ set , set , set ] means P1[\$1,\$2 `1 ,\$2 `2 ,\$3 `1 ,\$3 `2 ];
A2: for n being Nat
for x being Element of [:F1(),F2():] ex y being Element of [:F1(),F2():] st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of [:F1(),F2():] ex y being Element of [:F1(),F2():] st S1[n,x,y]
let x be Element of [:F1(),F2():]; :: thesis: ex y being Element of [:F1(),F2():] st S1[n,x,y]
consider ai being Element of F1(), bi being Element of F2() such that
A3: P1[n,x `1 ,x `2 ,ai,bi] by A1;
take [ai,bi] ; :: thesis: S1[n,x,[ai,bi]]
thus S1[n,x,[ai,bi]] by A3; :: thesis: verum
end;
consider f being sequence of [:F1(),F2():] such that
A4: f . 0 = [F3(),F4()] and
A5: for e being Nat holds S1[e,f . e,f . (e + 1)] from take pr1 f ; :: thesis: ex g being sequence of F2() st
( (pr1 f) . 0 = F3() & g . 0 = F4() & ( for n being Nat holds P1[n,(pr1 f) . n,g . n,(pr1 f) . (n + 1),g . (n + 1)] ) )

take pr2 f ; :: thesis: ( (pr1 f) . 0 = F3() & (pr2 f) . 0 = F4() & ( for n being Nat holds P1[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)] ) )
( [F3(),F4()] `1 = F3() & [F3(),F4()] `2 = F4() ) ;
hence ( (pr1 f) . 0 = F3() & (pr2 f) . 0 = F4() ) by ; :: thesis: for n being Nat holds P1[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)]
let i be Nat; :: thesis: P1[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 ;
i in NAT by ORDINAL1:def 12;
then ( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by ;
hence P1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A5, A6; :: thesis: verum