let x, y be Element of F₁(); :: thesis: ( F₂() reduces x,y implies P₁[x,y] )
given p being RedSequence of F₂() such that A4: p . 1 = x and
A5: p . (len p) = y ; :: according to REWRITE1:def 3 :: thesis: P₁[x,y]
defpred S₁[ Nat] means ( 1 + $1 <= len p implies P₁[x,p . (1 + $1)] );

A6: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: ( 1 + (i + 1) <= len p implies P₁[x,p . (1 + (i + 1))] )

A8: i + 1 >= 1 by NAT_1:11;
assume A9: 1 + (i + 1) <= len p ; :: thesis: P₁[x,p . (1 + (i + 1))]
1 + (i + 1) >= 1 by NAT_1:11;
then A10: 1 + (i + 1) in dom p by A9, FINSEQ_3:25;
i + 1 < len p by A9, NAT_1:13;
then i + 1 in dom p by A8, FINSEQ_3:25;
then A11: [(p . (i + 1)),(p . (1 + (i + 1)))] in F₂() by A10, REWRITE1:def 2;
then A12: p . (1 + (i + 1)) in F₁() by ZFMISC_1:87;
A13: p . (i + 1) in F₁() by A11, ZFMISC_1:87;
then P₁[p . (i + 1),p . (1 + (i + 1))] by A1, A11, A12;
hence P₁[x,p . (1 + (i + 1))] by A3, A7, A9, A13, A12, NAT_1:13; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

A14: S₁[ 0 ] by A2, A4;
A15: for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A6);
len p >= 0 + 1 by NAT_1:13;
then consider n being Nat such that
A16: len p = 1 + n by NAT_1:10;
thus P₁[x,y] by A5, A16, A15; :: thesis: verum