consider t being RedSequence of F3() such that
A4: ( t . 1 = F1() & t . (len t) = F2() ) by A2;
defpred S1[ Nat] means ( $1 in dom t implies P1[t . $1] );
A5: S1[ 0 ] by FINSEQ_3:24;
A6: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume A8: ( i + 1 in dom t & P1[t . (i + 1)] ) ; :: thesis: contradiction
per cases ( i = 0 or i > 0 ) by NAT_1:3;
suppose i > 0 ; :: thesis: contradiction
then consider j being Nat such that
A9: i = j + 1 by NAT_1:6;
( i <= i + 1 & i + 1 <= len t ) by A8, FINSEQ_3:25, NAT_1:11;
then A10: ( 1 <= i & i <= len t & rng t <> {} ) by A9, NAT_1:11, XXREAL_0:2;
then A11: ( i in dom t & 1 in dom t ) by FINSEQ_3:25, FINSEQ_3:32;
[(t . i),(t . (i + 1))] in F3() by A8, A11, REWRITE1:def 2;
hence contradiction by A3, A7, A8, A11, A4, A10, REWRITE1:17; :: thesis: verum
end;
end;
end;
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A5, A6);
 hence P1[F2()] by A4, FINSEQ_5:6; :: thesis: verum