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;
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():];
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
;
S1[n,x,y]
thus
S1[
n,
x,
y]
by A3;
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 RECDEF_1:sch 2(A2);
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 FUNCT_2:sch 8(A5);
A7:
now for n being Nat holds P1[n,f . n,f . (n + 1),f . (n + 2)]let n be
Nat;
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;
verum end;
take
f
; ( 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 A4, A10
;
hence
( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) )
by A11, A7; verum