defpred S1[ set , set , set ] means ( P1[\$1,\$2 `1 ,\$2 `2 ,\$3 `2 ] & \$2 `2 = \$3 `1 );
A2: for n being Nat
for x being Element of [:F1(),F1():] ex y being Element of [:F1(),F1():] st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of [:F1(),F1():] ex y being Element of [:F1(),F1():] st S1[n,x,y]
let x be Element of [:F1(),F1():]; :: thesis: ex y being Element of [:F1(),F1():] st S1[n,x,y]
set z = x `1 ;
set w = x `2 ;
reconsider z = x `1 , w = x `2 as Element of F1() ;
consider s being Element of F1() such that
A3: P1[n,z,w,s] by A1;
set y = [w,s];
reconsider y = [w,s] as Element of [:F1(),F1():] ;
take y ; :: thesis: S1[n,x,y]
thus S1[n,x,y] by A3; :: thesis: verum
end;
consider g being sequence of [:F1(),F1():] such that
A4: ( g . 0 = [F2(),F3()] & ( for n being Nat holds S1[n,g . n,g . (n + 1)] ) ) from deffunc H1( Nat) -> Element of F1() = (g . \$1) `1 ;
A5: for x being Element of NAT holds H1(x) in F1() ;
consider f being sequence of F1() such that
A6: for x being Element of NAT holds f . x = H1(x) from
A7: now :: thesis: for n being Nat holds P1[n,f . n,f . (n + 1),f . (n + 2)]
let n be Nat; :: thesis: P1[n,f . n,f . (n + 1),f . (n + 2)]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A8: f . n = (g . nn) `1 by A6;
S1[n + 1,g . (n + 1),g . ((n + 1) + 1)] by A4;
then A9: f . (n + 2) = (g . (n + 1)) `2 by A6;
f . (n + 1) = (g . (n + 1)) `1 by A6
.= (g . nn) `2 by A4 ;
hence P1[n,f . n,f . (n + 1),f . (n + 2)] by A4, A8, A9; :: thesis: verum
end;
take f ; :: thesis: ( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) )
A10: S1[ 0 ,g . 0,g . (0 + 1)] by A4;
A11: f . 0 = (g . 0) `1 by A6
.= F2() by A4 ;
f . 1 = (g . 1) `1 by A6
.= F3() by ;
hence ( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) ) by ; :: thesis: verum