let A be non empty set ; :: thesis: for D being non empty a_partition of A
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

let D be non empty a_partition of A; :: thesis: for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

let f be finite-support Function of A,REAL; :: thesis: for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

let s1 be one-to-one FinSequence of A; :: thesis: for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

let s2 be one-to-one FinSequence of D; :: thesis: ( rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) implies Sum ((D eqSumOf f) * s2) = Sum (f * s1) )

assume that
A1: rng s2 = (proj D) .: (rng s1) and
A2: for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ; :: thesis: Sum ((D eqSumOf f) * s2) = Sum (f * s1)
defpred S1[ Nat] means for t1 being one-to-one FinSequence of A
for t2 being one-to-one FinSequence of D st rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = \$1 holds
Sum ((D eqSumOf f) * t2) = Sum (f * t1);
A3: S1[ 0 ]
proof
let t1 be one-to-one FinSequence of A; :: thesis: for t2 being one-to-one FinSequence of D st rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = 0 holds
Sum ((D eqSumOf f) * t2) = Sum (f * t1)

let t2 be one-to-one FinSequence of D; :: thesis: ( rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = 0 implies Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume that
A4: rng t2 = (proj D) .: (rng t1) and
for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ; :: thesis: ( not len t2 = 0 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )
assume len t2 = 0 ; :: thesis: Sum ((D eqSumOf f) * t2) = Sum (f * t1)
then A5: t2 = <*> D ;
dom (proj D) = A by FUNCT_2:def 1;
then rng t1 c= dom (proj D) by FINSEQ_1:def 4;
then A6: t1 = <*> A by A5, A4;
thus Sum ((D eqSumOf f) * t2) = Sum (f * t1) by A5, A6; :: thesis: verum
end;
A7: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A8: S1[j] ; :: thesis: S1[j + 1]
let t1 be one-to-one FinSequence of A; :: thesis: for t2 being one-to-one FinSequence of D st rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = j + 1 holds
Sum ((D eqSumOf f) * t2) = Sum (f * t1)

let t2 be one-to-one FinSequence of D; :: thesis: ( rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = j + 1 implies Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume that
A9: rng t2 = (proj D) .: (rng t1) and
A10: for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ; :: thesis: ( not len t2 = j + 1 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )
assume A11: len t2 = j + 1 ; :: thesis: Sum ((D eqSumOf f) * t2) = Sum (f * t1)
then consider r2 being FinSequence of D, X being Element of D such that
A12: t2 = r2 ^ <*X*> by FINSEQ_2:19;
rng <*X*> = {X} by FINSEQ_1:38;
then rng r2 misses {X} by ;
then A13: not X in rng r2 by ZFMISC_1:48;
1 + (len r2) = j + 1 by ;
then A14: len r2 = j ;
reconsider r2 = r2 as one-to-one FinSequence of D by ;
set r1 = t1 - ((proj D) " {X});
A15: rng (t1 - ((proj D) " {X})) c= rng t1 by FINSEQ_3:66;
rng t1 c= A by FINSEQ_1:def 4;
then rng (t1 - ((proj D) " {X})) c= A by A15;
then reconsider r1 = t1 - ((proj D) " {X}) as FinSequence of A by FINSEQ_1:def 4;
reconsider r1 = r1 as one-to-one FinSequence of A by FINSEQ_3:87;
A16: rng r2 = (proj D) .: (rng r1)
proof
for x being object st x in rng r2 holds
x in (proj D) .: (rng r1)
proof
let x be object ; :: thesis: ( x in rng r2 implies x in (proj D) .: (rng r1) )
assume A17: x in rng r2 ; :: thesis: x in (proj D) .: (rng r1)
then x in rng t2 by ;
then consider w being object such that
A18: w in dom (proj D) and
A19: w in rng t1 and
A20: x = (proj D) . w by ;
not w in (proj D) " {X}
proof
assume w in (proj D) " {X} ; :: thesis: contradiction
then (proj D) . w in {X} by FUNCT_1:def 7;
then X in rng r2 by ;
hence contradiction by A13; :: thesis: verum
end;
then w in (rng t1) \ ((proj D) " {X}) by ;
then w in rng r1 by FINSEQ_3:65;
hence x in (proj D) .: (rng r1) by ; :: thesis: verum
end;
hence rng r2 c= (proj D) .: (rng r1) ; :: according to XBOOLE_0:def 10 :: thesis: (proj D) .: (rng r1) c= rng r2
for x being object st x in (proj D) .: (rng r1) holds
x in rng r2
proof
let x be object ; :: thesis: ( x in (proj D) .: (rng r1) implies x in rng r2 )
assume A21: x in (proj D) .: (rng r1) ; :: thesis: x in rng r2
then consider w being object such that
A22: w in dom (proj D) and
A23: w in rng r1 and
A24: x = (proj D) . w by FUNCT_1:def 6;
w in (rng t1) \ ((proj D) " {X}) by ;
then not w in (proj D) " {X} by XBOOLE_0:def 5;
then not x in {X} by ;
then A25: not x in rng <*X*> by FINSEQ_1:38;
x in (proj D) .: (rng t1) by ;
then x in (rng r2) \/ () by ;
hence x in rng r2 by ; :: thesis: verum
end;
hence (proj D) .: (rng r1) c= rng r2 ; :: thesis: verum
end;
for Y being Element of D st Y in rng r2 holds
eqSupport (f,Y) c= rng r1
proof
let Y be Element of D; :: thesis: ( Y in rng r2 implies eqSupport (f,Y) c= rng r1 )
assume A26: Y in rng r2 ; :: thesis: eqSupport (f,Y) c= rng r1
for x being object st x in eqSupport (f,Y) holds
x in rng r1
proof
let x be object ; :: thesis: ( x in eqSupport (f,Y) implies x in rng r1 )
assume A27: x in eqSupport (f,Y) ; :: thesis: x in rng r1
rng r2 c= rng t2 by ;
then eqSupport (f,Y) c= rng t1 by ;
then A28: x in rng t1 by A27;
not x in (proj D) " {X}
proof
assume x in (proj D) " {X} ; :: thesis: contradiction
then A29: ( x in dom (proj D) & (proj D) . x in {X} ) by FUNCT_1:def 7;
then reconsider y = x as Element of A ;
y in Y by ;
then (proj D) . y = Y by EQREL_1:65;
then X in rng r2 by ;
hence contradiction by A13; :: thesis: verum
end;
then x in (rng t1) \ ((proj D) " {X}) by ;
hence x in rng r1 by FINSEQ_3:65; :: thesis: verum
end;
hence eqSupport (f,Y) c= rng r1 ; :: thesis: verum
end;
then A30: Sum ((D eqSumOf f) * r2) = Sum (f * r1) by A16, A14, A8;
reconsider canEq = canFS (eqSupport (f,X)) as FinSequence of A by FINSEQ_2:24;
reconsider qt1 = r1 ^ canEq as FinSequence of A ;
for x being object holds not x in (rng r1) /\ (rng (canFS (eqSupport (f,X))))
proof
given x being object such that A31: x in (rng r1) /\ (rng (canFS (eqSupport (f,X)))) ; :: thesis: contradiction
x in rng (canFS (eqSupport (f,X))) by ;
then A32: x in eqSupport (f,X) by FUNCT_2:def 3;
then reconsider y = x as Element of A ;
y in X by ;
then A33: (proj D) . y = X by EQREL_1:65;
A34: x in rng r1 by ;
then x in A by ;
then x in dom (proj D) by FUNCT_2:def 1;
then (proj D) . x in (proj D) .: (rng r1) by ;
then X in rng r2 by ;
hence contradiction by A13; :: thesis: verum
end;
then rng r1 misses rng canEq by XBOOLE_0:def 1;
then reconsider qt1 = qt1 as one-to-one FinSequence of A by FINSEQ_3:91;
for x being object st x in rng qt1 holds
x in rng t1
proof end;
then A36: rng qt1 c= rng t1 ;
for x being Element of A st x in (rng t1) \ (rng qt1) holds
f . x = 0
proof
let x be Element of A; :: thesis: ( x in (rng t1) \ (rng qt1) implies f . x = 0 )
assume x in (rng t1) \ (rng qt1) ; :: thesis: f . x = 0
then A37: ( x in rng t1 & not x in rng qt1 ) by XBOOLE_0:def 5;
then not x in (rng r1) \/ (rng canEq) by FINSEQ_1:31;
then A38: ( not x in rng r1 & not x in rng (canFS (eqSupport (f,X))) ) by XBOOLE_0:def 3;
then not x in eqSupport (f,X) by FUNCT_2:def 3;
end;
then A41: Sum (f * qt1) = Sum (f * t1) by ;
thus Sum ((D eqSumOf f) * t2) = Sum (((D eqSumOf f) * r2) ^ <*((D eqSumOf f) . X)*>) by
.= (Sum (f * r1)) + ((D eqSumOf f) . X) by
.= (Sum (f * r1)) + (Sum (f * (canFS (eqSupport (f,X))))) by Def14
.= Sum ((f * r1) ^ (f * canEq)) by RVSUM_1:75
.= Sum (f * t1) by ; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A3, A7);
then S1[ len s2] ;
hence Sum ((D eqSumOf f) * s2) = Sum (f * s1) by A1, A2; :: thesis: verum