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

proof

let f be FinSequence of ; :: thesis: for p being Point of st S₁[f] holds
S₁[f ^ <*p*>]
let p be Point of ; :: 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:47
.= L~ (Rev <*p*>) by FINSEQ_5:63
.= L~ (Rev (f ^ <*p*>)) by A3, FINSEQ_1:47 ;
:: thesis: verum

end;

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

set q' = (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:68;
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:66 ;
:: thesis: verum

end;

end;

end;

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