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;
per cases ( A is empty or not A is empty ) ;
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;
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;
end;