let f be FinSequence; :: thesis: f = (Rev f) * (Rev (idseq (len f)))
reconsider P = Rev (idseq (len f)) as Permutation of (dom (Rev f)) by RFP;
reconsider g = (Rev f) * P as FinSequence ;
A1: dom f = dom (Rev f) by FINSEQ_5:57
.= dom ((Rev f) * P) by DR ;
for x being object st x in dom f holds
f . x = g . x
proof
set n = len f;
let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume B1: x in dom f ; :: thesis: f . x = g . x
reconsider x = x as Nat by B1;
B2: ( 1 <= x & x <= len f ) by B1, FINSEQ_3:25;
then reconsider m = x - 1 as Nat ;
reconsider k = (len f) - x as Element of NAT by B2, NAT_1:21;
set l = k + 1;
( 1 + 0 <= k + 1 & k + 1 <= k + x ) by B2, XREAL_1:6;
then k + 1 in dom f by FINSEQ_3:25;
then B3: k + 1 in dom (Rev f) by FINSEQ_5:57;
g . x = (Rev f) . ((Rev (idseq (m + (k + 1)))) . (m + 1)) by A1, B1, FUNCT_1:12
.= f . (((len f) - (k + 1)) + 1) by B3, FINSEQ_5:def 3
.= f . x ;
hence f . x = g . x ; :: thesis: verum
end;
hence f = (Rev f) * (Rev (idseq (len f))) by A1, FUNCT_1:2; :: thesis: verum