let f be FinSequence of (TOP-REAL 2); ( f is unfolded implies Rev f is unfolded )
assume A1:
f is unfolded
; Rev f is unfolded
A2:
dom f = Seg (len f)
by FINSEQ_1:def 3;
let i be Nat; TOPREAL1:def 6 ( not 1 <= i or not i + 2 <= len (Rev f) or (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))} )
assume that
A3:
1 <= i
and
A4:
i + 2 <= len (Rev f)
; (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))}
A5:
len (Rev f) = len f
by FINSEQ_5:def 3;
then A6:
i + 1 in dom f
by A3, A4, SEQ_4:135;
i + 1 <= (i + 1) + 1
by NAT_1:11;
then reconsider j9 = (len f) - (i + 1) as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;
i <= i + 2
by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;
A7:
j9 + (i + 1) = len f
;
i in dom f
by A3, A4, A5, SEQ_4:135;
then
j + 1 in dom f
by A2, FINSEQ_5:2;
then A8:
j9 + 2 <= len f
by FINSEQ_3:25;
A9:
j + (i + 1) = (len f) + 1
;
i + (1 + 1) = (i + 1) + 1
;
then A10:
1 <= j9
by A4, A5, XREAL_1:19;
j + i = len f
;
hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) =
(LSeg (f,j)) /\ (LSeg ((Rev f),(i + 1)))
by Th2
.=
(LSeg (f,(j9 + 1))) /\ (LSeg (f,j9))
by A7, Th2
.=
{(f /. (j9 + 1))}
by A1, A10, A8
.=
{((Rev f) /. (i + 1))}
by A9, A2, A6, FINSEQ_5:2, FINSEQ_5:66
;
verum