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

let p be Point of (); :: thesis: ( S1[f] implies S1[f ^ <*p*>] )
assume A2: S1[f] ; :: thesis: S1[f ^ <*p*>]
per cases ( f is empty or not f is empty ) ;
suppose A3: f is empty ; :: thesis: S1[f ^ <*p*>]
hence L~ (f ^ <*p*>) = L~ <*p*> by FINSEQ_1:34
.= L~ () by FINSEQ_5:60
.= L~ (Rev (f ^ <*p*>)) by ;
:: thesis: verum
end;
suppose A4: not f is empty ; :: thesis: S1[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 ;
hence L~ (f ^ <*p*>) = (LSeg (p,((Rev f) /. 1))) \/ (L~ (Rev f)) by A2, A4, Th19
.= L~ (<*p*> ^ (Rev f)) by
.= L~ (Rev (f ^ <*p*>)) by FINSEQ_5:63 ;
:: thesis: verum
end;
end;
end;
A6: S1[ <*> the carrier of ()] ;
for f being FinSequence of () holds S1[f] from hence L~ f = L~ (Rev f) ; :: thesis: verum