let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded implies Rev f is unfolded )

assume A1: f is unfolded ; :: thesis: Rev f is unfolded

A2: dom f = Seg (len f) by FINSEQ_1:def 3;

let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( 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) ; :: thesis: (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 ;

:: thesis: verum

assume A1: f is unfolded ; :: thesis: Rev f is unfolded

A2: dom f = Seg (len f) by FINSEQ_1:def 3;

let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( 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) ; :: thesis: (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 ;

:: thesis: verum