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 s1 = support f & rng s2 = support (D eqSumOf f) 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 s1 = support f & rng s2 = support (D eqSumOf f) 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 s1 = support f & rng s2 = support (D eqSumOf f) 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 s1 = support f & rng s2 = support (D eqSumOf f) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
let s2 be one-to-one FinSequence of D; :: thesis: ( rng s1 = support f & rng s2 = support (D eqSumOf f) implies Sum ((D eqSumOf f) * s2) = Sum (f * s1) )
assume that
A1: rng s1 = support f and
A2: rng s2 = support (D eqSumOf f) ; :: thesis: Sum ((D eqSumOf f) * s2) = Sum (f * s1)
A3: (proj D) .: (rng s1) c= rng (proj D) by RELAT_1:111;
rng (proj D) c= D by RELAT_1:def 19;
then (proj D) .: (rng s1) c= D by A3;
then reconsider s3 = canFS ((proj D) .: (rng s1)) as FinSequence of D by FINSEQ_2:24;
reconsider s3 = s3 as one-to-one FinSequence of D ;
A4: rng s3 = (proj D) .: (rng s1) by FUNCT_2:def 3;
for X being Element of D st X in rng s3 holds
eqSupport (f,X) c= rng s1 by A1, XBOOLE_0:def 4;
then A5: Sum ((D eqSumOf f) * s3) = Sum (f * s1) by A4, Th69;
support (D eqSumOf f) c= (proj D) .: (support f) by Th64;
then A6: rng s2 c= rng s3 by A1, A2, A4;
for X being Element of D st X in (rng s3) \ (rng s2) holds
(D eqSumOf f) . X = 0

proof

let X be Element of D; :: thesis: ( X in (rng s3) \ (rng s2) implies (D eqSumOf f) . X = 0 )
assume X in (rng s3) \ (rng s2) ; :: thesis: (D eqSumOf f) . X = 0
then not X in support (D eqSumOf f) by A2, XBOOLE_0:def 5;
hence (D eqSumOf f) . X = 0 by PRE_POLY:def 7; :: thesis: verum

end;

hence Sum ((D eqSumOf f) * s2) = Sum (f * s1) by A5, A6, Th9; :: thesis: verum