let F be Function of (),REAL; :: thesis: ( F = eqSumOf f iff for X being Element of () st X in the carrier of () holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) )

thus ( F = eqSumOf f implies for X being Element of () st X in the carrier of () holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) ) :: thesis: ( ( for X being Element of () st X in the carrier of () holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) ) implies F = eqSumOf f )
proof
assume F = eqSumOf f ; :: thesis: for X being Element of () st X in the carrier of () holds
F . X = Sum (f * (canFS (eqSupport (f,X))))

then consider D being a_partition of the carrier of A such that
A1: D = the carrier of () and
A2: F = D eqSumOf f by Def15;
let X be Element of (); :: thesis: ( X in the carrier of () implies F . X = Sum (f * (canFS (eqSupport (f,X)))) )
reconsider Y = X as Element of D by A1;
assume X in the carrier of () ; :: thesis: F . X = Sum (f * (canFS (eqSupport (f,X))))
hence F . X = Sum (f * (canFS (eqSupport (f,Y)))) by
.= Sum (f * (canFS (eqSupport (f,X)))) ;
:: thesis: verum
end;
assume A3: for X being Element of () st X in the carrier of () holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) ; :: thesis: F = eqSumOf f
dom F = the carrier of () by FUNCT_2:def 1;
then A4: dom F = dom () by FUNCT_2:def 1;
for x being object st x in dom F holds
F . x = () . x
proof
let x be object ; :: thesis: ( x in dom F implies F . x = () . x )
assume A5: x in dom F ; :: thesis: F . x = () . x
then reconsider X = x as Element of () ;
reconsider D = the carrier of () as a_partition of the carrier of A by Th47;
reconsider Y = X as Element of D ;
thus F . x = Sum (f * (canFS (eqSupport (f,X)))) by A3, A5
.= Sum (f * (canFS (eqSupport (f,Y))))
.= (D eqSumOf f) . Y by
.= () . x by Def15 ; :: thesis: verum
end;
hence F = eqSumOf f by ; :: thesis: verum