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 A14, FINSEQ_1:31;
{x} c= rng s by A8, ZFMISC_1:31;
then A17: rng (u ^ <*x*>) c= rng s by A16, XBOOLE_1:8;
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 Th1, FINSEQ_1:4;
then (Seg ((len u) + (len <*x*>))) \ (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 ( (u ^ <*x*>) . 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 A14, A11, FUNCT_1:def 3;
( 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 A19, FUNCT_1:47;
hence contradiction by A23, A24; :: thesis: verum
end;
assume A25: x2 in dom u ; :: thesis: contradiction
then u . x2 = (u ^ <*x*>) . x1 by A19, A22, FUNCT_1:47;
hence contradiction by A23, A25; :: thesis: verum
end;
then ( x1 in (dom (u ^ <*x*>)) \ (dom u) & x2 in (dom (u ^ <*x*>)) \ (dom u) ) by A20, A21, XBOOLE_0:def 5;
then {x1,x2} c= (dom (u ^ <*x*>)) \ (dom u) by ZFMISC_1:32;
then ( x1 = (len u) + 1 & x2 = (len u) + 1 ) by A18, ZFMISC_1:20;
hence x1 = x2 ; :: thesis: verum
end;
suppose A26: (u ^ <*x*>) . x1 <> x ; :: thesis: x1 = x2
A27: ( x1 in dom u & x2 in dom u ) then ( u . x1 = (u ^ <*x*>) . x1 & u . x2 = (u ^ <*x*>) . x2 ) by A19, FUNCT_1:47;
hence x1 = x2 by A22, A12, A27, FUNCT_1:def 4; :: 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 A14, A16, XBOOLE_1:7;
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 A8, A30;
reconsider x = x as Element of X by A8, A30;
{x} c= X by A8, A30, ZFMISC_1:31;
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 A31, FINSEQ_2:35
.= Sum (f * v) by A31, FINSEQOP:9 ;
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 A16, A28, A29; :: 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 A33, FUNCT_1:3;
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 FUNCT_2:sch 1(A35);
 Seg (len r) = Seg (len s) by A1, A32, A33, FINSEQ_1:48;
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 A39, A40;
r . i = s . (p . i) by A42, A37;
then r . i = r . j by A41, A42, A37;
hence i = j by A42, A32, FUNCT_1:def 4; :: thesis: verum
end;
then A43: p is one-to-one by FUNCT_1:def 4;
card (dom r) = card (dom s) by A38;
then p is onto by A43, FINSEQ_4:63;
hence p is Permutation of (dom r) by A43, A38; :: 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 A38, FUNCT_2:def 1; :: 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 A45, FUNCT_2:def 1; :: thesis: verum
end;
then s * p = r by A37, FUNCT_1:10;
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 FINSEQ_1:def 4, TARSKI:def 3;
then s . x in dom f by FUNCT_2:def 1;
hence x in dom (f * s) by A47, FUNCT_1:11; :: 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 A46, A48, RFINSEQ:4;
hence Sum (f * s) = Sum (f * t) by A34, RFINSEQ:9; :: thesis: verum