let f be FinSequence of (TOP-REAL 2); :: thesis: L~ f = L~ (Rev f)
defpred S₁[ FinSequence of (TOP-REAL 2)] means L~ $1 = L~ (Rev $1);
A1: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st S₁[f] holds
S₁[f ^ <*p*>]

proof

let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st S₁[f] holds
S₁[f ^ <*p*>]
let p be Point of (TOP-REAL 2); :: thesis: ( S₁[f] implies S₁[f ^ <*p*>] )
assume A2: S₁[f] ; :: thesis: S₁[f ^ <*p*>]

per cases ( f is empty or not f is empty ) ;

suppose A3: f is empty ; :: thesis: S₁[f ^ <*p*>]

hence L~ (f ^ <*p*>) = L~ <*p*> by FINSEQ_1:34
.= L~ (Rev <*p*>) by FINSEQ_5:60
.= L~ (Rev (f ^ <*p*>)) by A3, FINSEQ_1:34 ;
:: thesis: verum

end;

suppose A4: not f is empty ; :: thesis: S₁[f ^ <*p*>]

set q9 = (Rev f) /. 1;
set q = f /. (len f);
len f = len (Rev f) by FINSEQ_5:def 3;
then A5: not Rev f is empty by A4;
f /. (len f) = (Rev f) /. 1 by A4, FINSEQ_5:65;
hence L~ (f ^ <*p*>) = (LSeg (p,((Rev f) /. 1))) \/ (L~ (Rev f)) by A2, A4, Th19
.= L~ (<*p*> ^ (Rev f)) by A5, Th20
.= L~ (Rev (f ^ <*p*>)) by FINSEQ_5:63 ;
:: thesis: verum

end;

end;

end;

A6: S₁[ <*> the carrier of (TOP-REAL 2)] ;
for f being FinSequence of (TOP-REAL 2) holds S₁[f] from FINSEQ_2:sch 2(A6, A1);
hence L~ f = L~ (Rev f) ; :: thesis: verum