let X be set ; :: thesis: for s, t being FinSequence of X
for f being Function of X,REAL st s is one-to-one & t is one-to-one & rng t c= rng s & ( for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ) holds
Sum (f * s) = Sum (f * t)

let s, t be FinSequence of X; :: thesis: for f being Function of X,REAL st s is one-to-one & t is one-to-one & rng t c= rng s & ( for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ) holds
Sum (f * s) = Sum (f * t)

let f be Function of X,REAL; :: thesis: ( s is one-to-one & t is one-to-one & rng t c= rng s & ( for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ) implies Sum (f * s) = Sum (f * t) )

assume that
A1: s is one-to-one and
A2: t is one-to-one and
A3: rng t c= rng s and
A4: for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ; :: thesis: Sum (f * s) = Sum (f * t)
defpred S1[ set ] means ex r being FinSequence of X st
( r is one-to-one & rng t c= rng r & rng r = \$1 & Sum (f * r) = Sum (f * t) );
A5: rng s is finite ;
reconsider rngt = rng t as Subset of (rng s) by A3;
A6: S1[rngt] by A2;
A7: for x, C being set st x in (rng s) \ rngt & rngt c= C & C c= rng s & S1[C] holds
S1[C \/ {x}]
proof
let x, C be set ; :: thesis: ( x in (rng s) \ rngt & rngt c= C & C c= rng s & S1[C] implies S1[C \/ {x}] )
assume that
A8: x in (rng s) \ rngt and
rngt c= C and
A9: C c= rng s and
A10: S1[C] ; :: thesis: S1[C \/ {x}]
reconsider x = x as Element of rng s by A8;
reconsider C = C as Subset of (rng s) by A9;
per cases ( x in C or not x in C ) ;
suppose A11: not x in C ; :: thesis: S1[C \/ {x}]
consider u being FinSequence of X such that
A12: u is one-to-one and
A13: rngt c= rng u and
A14: rng u = C and
A15: Sum (f * u) = Sum (f * t) by A10;
set v = u ^ <*x*>;
rng <*x*> = {x} by FINSEQ_1:38;
then A16: rng (u ^ <*x*>) = C \/ {x} by ;
{x} c= rng s by ;
then A17: rng (u ^ <*x*>) c= rng s by ;
A18: (dom (u ^ <*x*>)) \ (dom u) = {((len u) + 1)}
proof
Seg (len u) = (Seg ((len u) + 1)) \ {((len u) + 1)} by FINSEQ_1:10;
then (Seg ((len u) + 1)) \ (Seg (len u)) = {((len u) + 1)} by ;
then (Seg ((len u) + ())) \ (Seg (len u)) = {((len u) + 1)} by FINSEQ_1:39;
then (Seg (len (u ^ <*x*>))) \ (Seg (len u)) = {((len u) + 1)} by FINSEQ_1:22;
then (dom (u ^ <*x*>)) \ (Seg (len u)) = {((len u) + 1)} by FINSEQ_1:def 3;
hence (dom (u ^ <*x*>)) \ (dom u) = {((len u) + 1)} by FINSEQ_1:def 3; :: thesis: verum
end;
A19: u = (u ^ <*x*>) | (dom u) by FINSEQ_1:21;
take u ^ <*x*> ; :: thesis: ( u ^ <*x*> is Element of K16(K17(NAT,X)) & u ^ <*x*> is FinSequence of X & u ^ <*x*> is one-to-one & rng t c= rng (u ^ <*x*>) & rng (u ^ <*x*>) = C \/ {x} & Sum (f * (u ^ <*x*>)) = Sum (f * t) )
for x1, x2 being object st x1 in dom (u ^ <*x*>) & x2 in dom (u ^ <*x*>) & (u ^ <*x*>) . x1 = (u ^ <*x*>) . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom (u ^ <*x*>) & x2 in dom (u ^ <*x*>) & (u ^ <*x*>) . x1 = (u ^ <*x*>) . x2 implies x1 = x2 )
assume that
A20: x1 in dom (u ^ <*x*>) and
A21: x2 in dom (u ^ <*x*>) and
A22: (u ^ <*x*>) . x1 = (u ^ <*x*>) . x2 ; :: thesis: x1 = x2
per cases ) . x1 = x or (u ^ <*x*>) . x1 <> x ) ;
suppose (u ^ <*x*>) . x1 = x ; :: thesis: x1 = x2
then A23: for y being object st y in dom u holds
(u ^ <*x*>) . x1 <> u . y by ;
( not x1 in dom u & not x2 in dom u )
proof
thus not x1 in dom u :: thesis: not x2 in dom u
proof
assume A24: x1 in dom u ; :: thesis: contradiction
then u . x1 = (u ^ <*x*>) . x1 by ;
hence contradiction by A23, A24; :: thesis: verum
end;
assume A25: x2 in dom u ; :: thesis: contradiction
then u . x2 = (u ^ <*x*>) . x1 by ;
hence contradiction by A23, A25; :: thesis: verum
end;
then ( x1 in (dom (u ^ <*x*>)) \ (dom u) & x2 in (dom (u ^ <*x*>)) \ (dom u) ) by ;
then {x1,x2} c= (dom (u ^ <*x*>)) \ (dom u) by ZFMISC_1:32;
then ( x1 = (len u) + 1 & x2 = (len u) + 1 ) by ;
hence x1 = x2 ; :: thesis: verum
end;
suppose A26: (u ^ <*x*>) . x1 <> x ; :: thesis: x1 = x2
A27: ( x1 in dom u & x2 in dom u )
proof
thus x1 in dom u :: thesis: x2 in dom u
proof
assume not x1 in dom u ; :: thesis: contradiction
then x1 in (dom (u ^ <*x*>)) \ (dom u) by ;
then x1 = (len u) + 1 by ;
hence contradiction by A26, FINSEQ_1:42; :: thesis: verum
end;
assume not x2 in dom u ; :: thesis: contradiction
then x2 in (dom (u ^ <*x*>)) \ (dom u) by ;
then x2 = (len u) + 1 by ;
hence contradiction by A26, A22, FINSEQ_1:42; :: thesis: verum
end;
then ( u . x1 = (u ^ <*x*>) . x1 & u . x2 = (u ^ <*x*>) . x2 ) by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
then A28: u ^ <*x*> is one-to-one by FUNCT_1:def 4;
rng u c= rng (u ^ <*x*>) by ;
then A29: rngt c= rng (u ^ <*x*>) by A13;
A30: rng s c= X by FINSEQ_1:def 4;
then rng (u ^ <*x*>) c= X by A17;
then reconsider v = u ^ <*x*> as FinSequence of X by FINSEQ_1:def 4;
A31: x in X by ;
reconsider x = x as Element of X by ;
{x} c= X by ;
then rng <*x*> c= X by FINSEQ_1:38;
then reconsider iks = <*x*> as FinSequence of X by FINSEQ_1:def 4;
reconsider fx = f * iks as FinSequence of REAL ;
Sum (f * t) = (Sum (f * u)) + 0 by A15
.= (Sum (f * u)) + (f . x) by A4, A8
.= Sum ((f * u) ^ <*(f . x)*>) by RVSUM_1:74
.= Sum ((f * u) ^ fx) by
.= Sum (f * v) by ;
hence ( u ^ <*x*> is Element of K16(K17(NAT,X)) & u ^ <*x*> is FinSequence of X & u ^ <*x*> is one-to-one & rng t c= rng (u ^ <*x*>) & rng (u ^ <*x*>) = C \/ {x} & Sum (f * (u ^ <*x*>)) = Sum (f * t) ) by ; :: thesis: verum
end;
end;
end;
S1[ rng s] from ORDERS_5:sch 1(A5, A6, A7);
then consider r being FinSequence of X such that
A32: r is one-to-one and
rng t c= rng r and
A33: rng r = rng s and
A34: Sum (f * r) = Sum (f * t) ;
defpred S2[ object , object ] means r . \$1 = s . \$2;
A35: for i being object st i in dom r holds
ex j being object st
( j in dom s & S2[i,j] )
proof
let i be object ; :: thesis: ( i in dom r implies ex j being object st
( j in dom s & S2[i,j] ) )

assume i in dom r ; :: thesis: ex j being object st
( j in dom s & S2[i,j] )

then r . i in rng s by ;
then consider j being object such that
A36: ( j in dom s & r . i = s . j ) by FUNCT_1:def 3;
take j ; :: thesis: ( j in dom s & S2[i,j] )
thus ( j in dom s & S2[i,j] ) by A36; :: thesis: verum
end;
consider p being Function of (dom r),(dom s) such that
A37: for x being object st x in dom r holds
S2[x,p . x] from Seg (len r) = Seg (len s) by ;
then dom r = Seg (len s) by FINSEQ_1:def 3;
then A38: dom r = dom s by FINSEQ_1:def 3;
p is Permutation of (dom r)
proof
for i, j being object st i in dom p & j in dom p & p . i = p . j holds
i = j
proof
let i, j be object ; :: thesis: ( i in dom p & j in dom p & p . i = p . j implies i = j )
assume that
A39: i in dom p and
A40: j in dom p and
A41: p . i = p . j ; :: thesis: i = j
A42: ( i in dom r & j in dom r ) by ;
r . i = s . (p . i) by ;
then r . i = r . j by ;
hence i = j by ; :: thesis: verum
end;
then A43: p is one-to-one by FUNCT_1:def 4;
card (dom r) = card (dom s) by A38;
then rng p = dom s by ;
then p is onto by FUNCT_2:def 3;
hence p is Permutation of (dom r) by ; :: thesis: verum
end;
then reconsider p = p as Permutation of (dom s) by A38;
for i being object holds
( i in dom r iff ( i in dom p & p . i in dom s ) )
proof
let i be object ; :: thesis: ( i in dom r iff ( i in dom p & p . i in dom s ) )
hereby :: thesis: ( i in dom p & p . i in dom s implies i in dom r )
assume i in dom r ; :: thesis: ( i in dom p & p . i in dom s )
hence i in dom p by ; :: thesis: p . i in dom s
then p . i in rng p by FUNCT_1:3;
hence p . i in dom s by FUNCT_2:def 3; :: thesis: verum
end;
assume that
A45: i in dom p and
p . i in dom s ; :: thesis: i in dom r
thus i in dom r by ; :: thesis: verum
end;
then s * p = r by ;
then A46: (f * s) * p = f * r by RELAT_1:36;
for x being object holds
( x in dom (f * s) iff x in dom s )
proof
let x be object ; :: thesis: ( x in dom (f * s) iff x in dom s )
thus ( x in dom (f * s) implies x in dom s ) by FUNCT_1:11; :: thesis: ( x in dom s implies x in dom (f * s) )
assume A47: x in dom s ; :: thesis: x in dom (f * s)
then s . x in rng s by FUNCT_1:3;
then s . x in X by ;
then s . x in dom f by FUNCT_2:def 1;
hence x in dom (f * s) by ; :: thesis: verum
end;
then A48: dom (f * s) = dom s by TARSKI:2;
then reconsider p = p as Permutation of (dom (f * s)) ;
f * s,f * r are_fiberwise_equipotent by ;
hence Sum (f * s) = Sum (f * t) by ; :: thesis: verum