let cF be complex-valued XFinSequence; :: thesis: Sum cF = Sum (Rev cF)
reconsider Fr2 = cF, Fr1 = Rev cF as XFinSequence of COMPLEX ;
A1: len Fr1 = len Fr2 by Def1;
defpred S₁[ object , object ] means for i being Nat st i = $1 holds
$2 = (len Fr1) - (1 + i);
A2: card (len Fr1) = card (len Fr1) ;
A3: for x being object st x in len Fr1 holds
ex y being object st
( y in len Fr1 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in len Fr1 implies ex y being object st
( y in len Fr1 & S₁[x,y] ) )
assume A4: x in len Fr1 ; :: thesis: ex y being object st
( y in len Fr1 & S₁[x,y] )
reconsider k = x as Element of NAT by Th1, A4;
k + 1 <= len Fr1 by NAT_1:13, A4, AFINSQ_1:86;
then A5: (len Fr1) -' (1 + k) = (len Fr1) - (1 + k) by XREAL_1:233;
take (len Fr1) -' (1 + k) ; :: thesis: ( (len Fr1) -' (1 + k) in len Fr1 & S₁[x,(len Fr1) -' (1 + k)] )
(len Fr1) + zz < (len Fr1) + (1 + k) by XREAL_1:8;
then (len Fr1) - (1 + k) < ((len Fr1) + (1 + k)) - (1 + k) by XREAL_1:9;
hence ( (len Fr1) -' (1 + k) in len Fr1 & S₁[x,(len Fr1) -' (1 + k)] ) by A5, AFINSQ_1:86; :: thesis: verum

end;

consider P being Function of (len Fr1),(len Fr1) such that
A6: for x being object st x in len Fr1 holds
S₁[x,P . x] from FUNCT_2:sch 1(A3);
for x1, x2 being object st x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 implies x1 = x2 )
assume that
A7: x1 in len Fr1 and
A8: x2 in len Fr1 and
A9: P . x1 = P . x2 ; :: thesis: x1 = x2
reconsider i = x1, j = x2 as Element of NAT by A7, A8, Th1;
A10: P . x2 = (len Fr1) - (1 + j) by A6, A8;
P . x1 = (len Fr1) - (1 + i) by A6, A7;
hence x1 = x2 by A9, A10; :: thesis: verum

end;

then A11: P is one-to-one by FUNCT_2:56;
then P is onto by A2, Lm1;
then reconsider P = P as Permutation of (dom Fr1) by A11;

A12: now :: thesis: for x being object st x in dom Fr1 holds
Fr1 . x = Fr2 . (P . x)

let x be object ; :: thesis: ( x in dom Fr1 implies Fr1 . x = Fr2 . (P . x) )
assume A13: x in dom Fr1 ; :: thesis: Fr1 . x = Fr2 . (P . x)
reconsider k = x as Element of NAT by A13;
P . k = (len Fr1) - (1 + k) by A6, A13;
hence Fr1 . x = Fr2 . (P . x) by A1, Def1, A13; :: thesis: verum

end;

A14: now :: thesis: for x being object st x in dom Fr1 holds
( x in dom P & P . x in dom Fr2 )

let x be object ; :: thesis: ( x in dom Fr1 implies ( x in dom P & P . x in dom Fr2 ) )
assume A15: x in dom Fr1 ; :: thesis: ( x in dom P & P . x in dom Fr2 )
x in dom P by A15, FUNCT_2:52;
then P . x in rng P by FUNCT_1:3;
hence ( x in dom P & P . x in dom Fr2 ) by A1, A15, FUNCT_2:52; :: thesis: verum

end;

for x being object st x in dom P & P . x in dom Fr2 holds
x in dom Fr1 ;
then Fr1 = Fr2 * P by A14, A12, FUNCT_1:10;
hence Sum cF = Sum (Rev cF) by A1, Th44; :: thesis: verum