theorem Th60: :: ORDERS_5:49

for A being Preorder
for f being finite-support Function of A,REAL
for x being Element of A st ( for y being Element of A st x =~ y holds
x = y ) holds
((eqSumOf f) * (proj A)) . x = f . x