let A be Order; :: thesis: for f being finite-support Function of A,REAL holds (eqSumOf f) * (proj A) = f
let f be finite-support Function of A,REAL; :: thesis: (eqSumOf f) * (proj A) = f
set F = (eqSumOf f) * (proj A);
( QuotientOrder A is empty implies A is empty ) ;
then dom ((eqSumOf f) * (proj A)) = the carrier of A by FUNCT_2:def 1;
then A1: dom f = dom ((eqSumOf f) * (proj A)) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = ((eqSumOf f) * (proj A)) . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = ((eqSumOf f) * (proj A)) . x )
assume x in dom f ; :: thesis: f . x = ((eqSumOf f) * (proj A)) . x
then reconsider z = x as Element of A ;
for y being Element of A st z =~ y holds
z = y by ORDERS_2:2;
hence f . x = ((eqSumOf f) * (proj A)) . x by Th60; :: thesis: verum
end;
hence (eqSumOf f) * (proj A) = f by A1, FUNCT_1:2; :: thesis: verum