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 S_{1}[ 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: S_{1}[rngt]
by A2;

A7: for x, C being set st x in (rng s) \ rngt & rngt c= C & C c= rng s & S_{1}[C] holds

S_{1}[C \/ {x}]
_{1}[ 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 S_{2}[ 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 & S_{2}[i,j] )

A37: for x being object st x in dom r holds

S_{2}[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)

for i being object holds

( i in dom r iff ( i in dom p & p . i in dom s ) )

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 )

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

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 S

( 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: S

A7: for x, C being set st x in (rng s) \ rngt & rngt c= C & C c= rng s & S

S

proof

S
let x, C be set ; :: thesis: ( x in (rng s) \ rngt & rngt c= C & C c= rng s & S_{1}[C] implies S_{1}[C \/ {x}] )

assume that

A8: x in (rng s) \ rngt and

rngt c= C and

A9: C c= rng s and

A10: S_{1}[C]
; :: thesis: S_{1}[C \/ {x}]

reconsider x = x as Element of rng s by A8;

reconsider C = C as Subset of (rng s) by A9;

end;assume that

A8: x in (rng s) \ rngt and

rngt c= C and

A9: C c= rng s and

A10: S

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 )
;

end;

suppose A11:
not x in C
; :: thesis: S_{1}[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)}

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

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;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

A19:
u = (u ^ <*x*>) | (dom u)
by FINSEQ_1:21;
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;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

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

then A28:
u ^ <*x*> is one-to-one
by FUNCT_1:def 4;
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

end;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 )
;

end;

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 )

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;(u ^ <*x*>) . x1 <> u . y by A14, A11, FUNCT_1:def 3;

( not x1 in dom u & not x2 in dom u )

proof

then
( x1 in (dom (u ^ <*x*>)) \ (dom u) & x2 in (dom (u ^ <*x*>)) \ (dom u) )
by A20, A21, XBOOLE_0:def 5;
thus
not x1 in dom u
:: thesis: not x2 in dom u

then u . x2 = (u ^ <*x*>) . x1 by A19, A22, FUNCT_1:47;

hence contradiction by A23, A25; :: thesis: verum

end;proof

assume A25:
x2 in dom u
; :: thesis: contradiction
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;then u . x1 = (u ^ <*x*>) . x1 by A19, FUNCT_1:47;

hence contradiction by A23, A24; :: thesis: verum

then u . x2 = (u ^ <*x*>) . x1 by A19, A22, FUNCT_1:47;

hence contradiction by A23, A25; :: thesis: verum

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

suppose A26:
(u ^ <*x*>) . x1 <> x
; :: thesis: x1 = x2

A27:
( x1 in dom u & x2 in dom u )

hence x1 = x2 by A22, A12, A27, FUNCT_1:def 4; :: thesis: verum

end;proof

then
( u . x1 = (u ^ <*x*>) . x1 & u . x2 = (u ^ <*x*>) . x2 )
by A19, FUNCT_1:47;
thus
x1 in dom u
:: thesis: x2 in dom u

then x2 in (dom (u ^ <*x*>)) \ (dom u) by A21, XBOOLE_0:def 5;

then x2 = (len u) + 1 by A18, TARSKI:def 1;

hence contradiction by A26, A22, FINSEQ_1:42; :: thesis: verum

end;proof

assume
not x2 in dom u
; :: thesis: contradiction
assume
not x1 in dom u
; :: thesis: contradiction

then x1 in (dom (u ^ <*x*>)) \ (dom u) by A20, XBOOLE_0:def 5;

then x1 = (len u) + 1 by A18, TARSKI:def 1;

hence contradiction by A26, FINSEQ_1:42; :: thesis: verum

end;then x1 in (dom (u ^ <*x*>)) \ (dom u) by A20, XBOOLE_0:def 5;

then x1 = (len u) + 1 by A18, TARSKI:def 1;

hence contradiction by A26, FINSEQ_1:42; :: thesis: verum

then x2 in (dom (u ^ <*x*>)) \ (dom u) by A21, XBOOLE_0:def 5;

then x2 = (len u) + 1 by A18, TARSKI:def 1;

hence contradiction by A26, A22, FINSEQ_1:42; :: thesis: verum

hence x1 = x2 by A22, A12, A27, FUNCT_1:def 4; :: thesis: verum

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

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 S

A35: for i being object st i in dom r holds

ex j being object st

( j in dom s & S

proof

consider p being Function of (dom r),(dom s) such that
let i be object ; :: thesis: ( i in dom r implies ex j being object st

( j in dom s & S_{2}[i,j] ) )

assume i in dom r ; :: thesis: ex j being object st

( j in dom s & S_{2}[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 & S_{2}[i,j] )

thus ( j in dom s & S_{2}[i,j] )
by A36; :: thesis: verum

end;( j in dom s & S

assume i in dom r ; :: thesis: ex j being object st

( j in dom s & S

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 & S

thus ( j in dom s & S

A37: for x being object st x in dom r holds

S

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

then reconsider p = p as Permutation of (dom s) by A38;
for i, j being object st i in dom p & j in dom p & p . i = p . j holds

i = j

card (dom r) = card (dom s) by A38;

then rng p = dom s by A43, FINSEQ_4:63;

then p is onto by FUNCT_2:def 3;

hence p is Permutation of (dom r) by A43, A38; :: thesis: verum

end;i = j

proof

then A43:
p is one-to-one
by FUNCT_1:def 4;
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;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

card (dom r) = card (dom s) by A38;

then rng p = dom s by A43, FINSEQ_4:63;

then p is onto by FUNCT_2:def 3;

hence p is Permutation of (dom r) by A43, A38; :: thesis: verum

for i being object holds

( i in dom r iff ( i in dom p & p . i in dom s ) )

proof

then
s * p = r
by A37, FUNCT_1:10;
let i be object ; :: thesis: ( i in dom r iff ( i in dom p & p . i in dom s ) )

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;hereby :: thesis: ( i in dom p & p . i in dom s implies i in dom r )

assume that 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;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

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

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

then A48:
dom (f * s) = dom s
by TARSKI:2;
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;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

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