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;
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():];
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]
;
S1[n,x,[ai,bi]]
thus
S1[
n,
x,
[ai,bi]]
by A3;
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 RECDEF_1:sch 2(A2);
take
pr1 f
; 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
; ( (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 A4, FUNCT_2:def 5, FUNCT_2:def 6; 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; 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 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
P1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
by A5, A6; verum