let A be Preorder; :: 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 (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((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 (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((eqSumOf f) * s2) = Sum (f * s1)

let s1 be one-to-one FinSequence of A; :: thesis: for s2 being one-to-one FinSequence of (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((eqSumOf f) * s2) = Sum (f * s1)

let s2 be one-to-one FinSequence of (QuotientOrder A); :: thesis: ( rng s1 = support f & rng s2 = support (eqSumOf f) implies Sum ((eqSumOf f) * s2) = Sum (f * s1) )

assume that

A1: rng s1 = support f and

A2: rng s2 = support (eqSumOf f) ; :: thesis: Sum ((eqSumOf f) * s2) = Sum (f * s1)

consider D being a_partition of the carrier of A such that

A3: D = the carrier of (QuotientOrder A) and

A4: D eqSumOf f = eqSumOf f by Def15;

for s1 being one-to-one FinSequence of A

for s2 being one-to-one FinSequence of (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((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 (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((eqSumOf f) * s2) = Sum (f * s1)

let s1 be one-to-one FinSequence of A; :: thesis: for s2 being one-to-one FinSequence of (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds

Sum ((eqSumOf f) * s2) = Sum (f * s1)

let s2 be one-to-one FinSequence of (QuotientOrder A); :: thesis: ( rng s1 = support f & rng s2 = support (eqSumOf f) implies Sum ((eqSumOf f) * s2) = Sum (f * s1) )

assume that

A1: rng s1 = support f and

A2: rng s2 = support (eqSumOf f) ; :: thesis: Sum ((eqSumOf f) * s2) = Sum (f * s1)

consider D being a_partition of the carrier of A such that

A3: D = the carrier of (QuotientOrder A) and

A4: D eqSumOf f = eqSumOf f by Def15;

per cases
( A is empty or not A is empty )
;

end;

suppose
A is empty
; :: thesis: Sum ((eqSumOf f) * s2) = Sum (f * s1)

then
( eqSumOf f is empty & f is empty )
;

hence Sum ((eqSumOf f) * s2) = Sum (f * s1) ; :: thesis: verum

end;hence Sum ((eqSumOf f) * s2) = Sum (f * s1) ; :: thesis: verum

suppose
not A is empty
; :: thesis: Sum ((eqSumOf f) * s2) = Sum (f * s1)

then reconsider B = A as non empty Preorder ;

reconsider E = D as non empty a_partition of the carrier of B ;

reconsider s3 = s2 as one-to-one FinSequence of E by A3;

reconsider F = f as finite-support Function of B,REAL ;

rng s3 = support (E eqSumOf F) by A2, A4;

hence Sum ((eqSumOf f) * s2) = Sum (f * s1) by A1, A4, Th70; :: thesis: verum

end;reconsider E = D as non empty a_partition of the carrier of B ;

reconsider s3 = s2 as one-to-one FinSequence of E by A3;

reconsider F = f as finite-support Function of B,REAL ;

rng s3 = support (E eqSumOf F) by A2, A4;

hence Sum ((eqSumOf f) * s2) = Sum (f * s1) by A1, A4, Th70; :: thesis: verum