let A be non empty set ; 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; 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; 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; 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; ( 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)
; 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
hence
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
by A5, A6, Th9; verum