let Fr1, Fr2 be XFinSequence of ; :: thesis: ( 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)) ; :: thesis: Sum Fr1 = Sum Fr2
defpred S₁[ set , set ] 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 set st x in len Fr1 holds
ex y being set st
( y in len Fr1 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in len Fr1 implies ex y being set st
( y in len Fr1 & S₁[x,y] ) )
assume A5: x in len Fr1 ; :: thesis: ex y being set st
( y in len Fr1 & S₁[x,y] )
len Fr1 is Subset of NAT by STIRL2_1:8;
then reconsider k = x as Element of NAT by A5;
k < len Fr1 by A5, NAT_1:44;
then k + 1 <= len Fr1 by NAT_1:13;
then A6: (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) + 0 < (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 A6, NAT_1:44; :: thesis: verum

end;

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

proof

let x1, x2 be set ; :: thesis: ( x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 implies x1 = x2 )
assume that
A9: x1 in len Fr1 and
A10: x2 in len Fr1 and
A11: P . x1 = P . x2 ; :: thesis: x1 = x2
len Fr1 is Subset of NAT by STIRL2_1:8;
then reconsider i = x1, j = x2 as Element of NAT by A9, A10;
j < len Fr1 by A10, NAT_1:44;
then j + 1 <= len Fr1 by NAT_1:13;
then (len Fr1) -' (1 + j) = (len Fr1) - (1 + j) by XREAL_1:233;
then A12: P . x2 = (len Fr1) - (1 + j) by A7, A10;
i < len Fr1 by A9, NAT_1:44;
then i + 1 <= len Fr1 by NAT_1:13;
then (len Fr1) -' (1 + i) = (len Fr1) - (1 + i) by XREAL_1:233;
then P . x1 = (len Fr1) - (1 + i) by A7, A9;
hence x1 = x2 by A11, A12; :: thesis: verum

end;

then A13: P is one-to-one by FUNCT_2:56;
P is one-to-one by A8, FUNCT_2:56;
then P is onto by A3, STIRL2_1:60;
then reconsider P = P as Permutation of (dom Fr1) by A13;

A14: now

let x be set ; :: thesis: ( x in dom Fr1 implies Fr1 . x = Fr2 . (P . x) )
assume A15: x in dom Fr1 ; :: thesis: Fr1 . x = Fr2 . (P . x)
reconsider k = x as Element of NAT by A15;
P . k = (len Fr1) -' (1 + k) by A7, A15;
hence Fr1 . x = Fr2 . (P . x) by A2, A15; :: thesis: verum

end;

A16: for x being set st x in dom Fr1 holds
( x in dom P & P . x in dom Fr2 ) by A1, FUNCT_2:52;
for x being set st x in dom P & P . x in dom Fr2 holds
x in dom Fr1 ;
then Fr1 = Fr2 * P by A16, A14, 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; :: thesis: verum