let X be set ; :: thesis:
let s, t be FinSequence of X; :: thesis:
let f be Function of X,REAL; :: thesis:
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:
defpred S₁[ 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₁[rngt] by A2;
A7: for x, C being set st x in (rng s) \ rngt & rngt c= C & C c= rng s & S₁[C] holds
S₁[C \/ {x}]

proof

let x, C be set ; :: thesis:
assume that
A8: x in (rng s) \ rngt and
rngt c= C and
A9: C c= rng s and
A10: S₁[C] ; :: thesis:
reconsider x = x as Element of rng s by A8;
reconsider C = C as Subset of (rng s) by A9;

per cases ;

suppose x in C ; :: thesis:

then C = C \/ {x} by ZFMISC_1:40;
hence S₁[C \/ {x}] by A10; :: thesis:

end;

suppose A11: not x in C ; :: thesis:

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:

end;

A19: u = (u ^ <*x*>) | (dom u) by FINSEQ_1:21;
take u ^ <*x*> ; :: thesis:
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:
assume that
A20: x1 in dom (u ^ <*x*>) and
A21: x2 in dom (u ^ <*x*>) and
A22: (u ^ <*x*>) . x1 = (u ^ <*x*>) . x2 ; :: thesis:

per cases ) . x1 = x or (u ^ <*x*>) . x1 <> x ) ;

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

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:

proof

assume A24: x1 in dom u ; :: thesis:
then u . x1 = (u ^ <*x*>) . x1 by A19, FUNCT_1:47;
hence contradiction by A23, A24; :: thesis:

end;

assume A25: x2 in dom u ; :: thesis:
then u . x2 = (u ^ <*x*>) . x1 by A19, A22, FUNCT_1:47;
hence contradiction by A23, A25; :: thesis:

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:

end;

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

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

proof

thus x1 in dom u :: thesis:

proof

assume not x1 in dom u ; :: thesis:
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:

end;

assume not x2 in dom u ; :: thesis:
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:

end;

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:

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:

end;

S₁[ 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₂[ 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₂[i,j] )

proof

let i be object ; :: thesis:
assume i in dom r ; :: thesis:
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:
thus ( j in dom s & S₂[i,j] ) by A36; :: thesis:

end;

consider p being Function of (dom r),(dom s) such that
A37: for x being object st x in dom r holds
S₂[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:
assume that
A39: i in dom p and
A40: j in dom p and
A41: p . i = p . j ; :: thesis:
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:

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:

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:

hereby :: thesis:

assume i in dom r ; :: thesis:
hence i in dom p by A38, FUNCT_2:def 1; :: thesis:
then p . i in rng p by FUNCT_1:3;
hence p . i in dom s by FUNCT_2:def 3; :: thesis:

end;

assume that
A45: i in dom p and
p . i in dom s ; :: thesis:
thus i in dom r by A45, FUNCT_2:def 1; :: thesis:

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:
thus ( x in dom (f * s) implies x in dom s ) by FUNCT_1:11; :: thesis:
assume A47: x in dom s ; :: thesis:
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:

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: