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: S₁[ <*> the carrier of (TOP-REAL 2)] ;
A2: 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 A3: S₁[f] ; :: thesis: S₁[f ^ <*p*>]

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

suppose A4: 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 A4, FINSEQ_1:47 ;
:: thesis: verum

end;

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

then A6: len f <> 0 ;
set q = f /. (len f);
A7: len f = len (Rev f) by FINSEQ_5:def 3;
set q' = (Rev f) /. 1;
A8: f /. (len f) = (Rev f) /. 1 by A5, FINSEQ_5:68;
A9: not Rev f is empty by A6, A7;
thus L~ (f ^ <*p*>) = (LSeg p,((Rev f) /. 1)) \/ (L~ (Rev f)) by A3, A5, A8, Th19
.= L~ (<*p*> ^ (Rev f)) by A9, Th20
.= L~ (Rev (f ^ <*p*>)) by FINSEQ_5:66 ; :: thesis: verum

end;

end;

end;

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