let A be Order; :: thesis: for f1, f2 being finite-support Function of A,REAL st eqSumOf f1 = eqSumOf f2 holds
f1 = f2
let f1, f2 be finite-support Function of A,REAL; :: thesis: ( eqSumOf f1 = eqSumOf f2 implies f1 = f2 )
assume A1: eqSumOf f1 = eqSumOf f2 ; :: thesis: f1 = f2
thus f1 = (eqSumOf f2) * (proj A) by A1, Th61
.= f2 by Th61 ; :: thesis: verum