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

proof

assume F = eqSumOf f ; :: thesis: for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) 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 (QuotientOrder A) and
A2: F = D eqSumOf f by Def15;
let X be Element of (QuotientOrder A); :: thesis: ( X in the carrier of (QuotientOrder A) implies F . X = Sum (f * (canFS (eqSupport (f,X)))) )
reconsider Y = X as Element of D by A1;
assume X in the carrier of (QuotientOrder A) ; :: thesis: F . X = Sum (f * (canFS (eqSupport (f,X))))
hence F . X = Sum (f * (canFS (eqSupport (f,Y)))) by A2, A1, Def14
.= Sum (f * (canFS (eqSupport (f,X)))) ;
:: thesis: verum

end;

assume A3: for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) ; :: thesis: F = eqSumOf f
dom F = the carrier of (QuotientOrder A) by FUNCT_2:def 1;
then A4: dom F = dom (eqSumOf f) by FUNCT_2:def 1;
for x being object st x in dom F holds
F . x = (eqSumOf f) . x

proof

let x be object ; :: thesis: ( x in dom F implies F . x = (eqSumOf f) . x )
assume A5: x in dom F ; :: thesis: F . x = (eqSumOf f) . x
then reconsider X = x as Element of (QuotientOrder A) ;
reconsider D = the carrier of (QuotientOrder A) 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 A5, Def14
.= (eqSumOf f) . x by Def15 ; :: thesis: verum

end;

hence F = eqSumOf f by A4, FUNCT_1:2; :: thesis: verum