consider t being RedSequence of F₄() such that
A1: ( t . 1 = F₂() & t . (len t) = F₃() ) by W2, REWRITE1:def 3;
reconsider t = t as F₁() -valued RedSequence of F₄() by A1, Lem2;
defpred S₁[ Nat] means ( $1 in dom t implies P₁[t . $1] );
A2: S₁[ 0 ] by FINSEQ_3:24;

A3: now

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

proof

assume A5: ( i + 1 in dom t & P₁[t . (i + 1)] ) ; :: thesis: contradiction
( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A6: i = j + 1 by W1, A1, A5, NAT_1:6;
( i <= i + 1 & i + 1 <= len t ) by A5, FINSEQ_3:25, NAT_1:11;
then A9: ( 1 <= i & i <= len t & rng t <> {} ) by A6, NAT_1:11, XXREAL_0:2;
then A7: ( i in dom t & 1 in dom t ) by FINSEQ_3:25, FINSEQ_3:32;
A8: ( t . i = t /. i & t . (i + 1) = t /. (i + 1) ) by A5, A7, PARTFUN1:def 6;
then [(t /. i),(t /. (i + 1))] in F₄() by A5, A7, REWRITE1:def 2;
hence contradiction by W3, A4, A5, A7, A1, A9, A8, REWRITE1:17; :: thesis: verum

end;

end;

BB: for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
len t in dom t by FINSEQ_5:6;
hence P₁[F₃()] by A1, BB; :: thesis: verum