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

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

hence
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
by A5, A6, Th9; :: thesis: verum
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;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