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 )

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

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 A3:
for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds
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;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

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

hence
F = eqSumOf f
by A4, FUNCT_1:2; :: thesis: verum
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;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