let Fr1, Fr2 be XFinSequence of REAL ; ( dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds
Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) implies Sum Fr1 = Sum Fr2 )
assume that
A1:
dom Fr1 = dom Fr2
and
A2:
for n being Nat st n in len Fr1 holds
Fr1 . n = Fr2 . ((len Fr1) -' (1 + n))
; Sum Fr1 = Sum Fr2
defpred S1[ object , object ] means for i being Nat st i = $1 holds
$2 = (len Fr1) -' (1 + i);
A3:
card (len Fr1) = card (len Fr1)
;
A4:
for x being object st x in len Fr1 holds
ex y being object st
( y in len Fr1 & S1[x,y] )
consider P being Function of (len Fr1),(len Fr1) such that
A7:
for x being object st x in len Fr1 holds
S1[x,P . x]
from FUNCT_2:sch 1(A4);
for x1, x2 being object st x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 holds
x1 = x2
then A12:
P is one-to-one
by FUNCT_2:56;
then
P is onto
by A3, FINSEQ_4:63;
then reconsider P = P as Permutation of (dom Fr1) by A12;
A15:
for x being object st x in dom Fr1 holds
( x in dom P & P . x in dom Fr2 )
for x being object st x in dom P & P . x in dom Fr2 holds
x in dom Fr1
;
then
Fr1 = Fr2 * P
by A15, A13, FUNCT_1:10;
then addreal "**" Fr1 =
addreal "**" Fr2
by A1, AFINSQ_2:45
.=
Sum Fr2
by AFINSQ_2:48
;
hence
Sum Fr1 = Sum Fr2
by AFINSQ_2:48; verum