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 8 ( 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, GOBOARD2:4;
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:18, 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:18, XXREAL_0:2;
A7:
j9 + (i + 1) = len f
;
i in dom f
by A3, A4, A5, GOBOARD2:4;
then
j + 1 in dom f
by A2, FINSEQ_5:2;
then A8:
j9 + 2 <= len f
by FINSEQ_3:27;
A9:
j + (i + 1) = (len f) + 1
;
i + (1 + 1) = (i + 1) + 1
;
then A10:
1 <= j9
by A4, A5, XREAL_1:21;
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, TOPREAL1:def 8
.=
{((Rev f) /. (i + 1))}
by A9, A2, A6, FINSEQ_5:2, FINSEQ_5:69
;
verum