consider t being RedSequence of F4() such that
A4:
( t . 1 = F2() & t . (len t) = F3() )
by A2;
reconsider t = t as F1() -valued RedSequence of F4() by A4, Th23;
defpred S1[ Nat] means ( $1 in dom t implies P1[t . $1] );
A5:
S1[ 0 ]
by FINSEQ_3:24;
A6:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A7:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verumproof
assume A8:
(
i + 1
in dom t &
P1[
t . (i + 1)] )
;
contradiction
(
i = 0 or
i >= 0 + 1 )
by NAT_1:13;
then consider j being
Nat such that A9:
i = j + 1
by A1, A4, A8, 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;
A12:
(
t . i = t /. i &
t . (i + 1) = t /. (i + 1) )
by A8, A11, PARTFUN1:def 6;
then
[(t /. i),(t /. (i + 1))] in F4()
by A8, A11, REWRITE1:def 2;
hence
contradiction
by A3, A7, A8, A11, A4, A10, A12, REWRITE1:17;
verum
end; end;
A13:
for i being Nat holds S1[i]
from NAT_1:sch 2(A5, A6);
len t in dom t
by FINSEQ_5:6;
hence
P1[F3()]
by A4, A13; verum