let A be Preorder; :: thesis: 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

let f be finite-support Function of A,REAL; :: thesis: 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

let x be Element of A; :: thesis: ( ( for y being Element of A st x =~ y holds

x = y ) implies ((eqSumOf f) * (proj A)) . x = f . x )

assume A1: for y being Element of A st x =~ y holds

x = y ; :: thesis: ((eqSumOf f) * (proj A)) . x = f . x

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

let f be finite-support Function of A,REAL; :: thesis: 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

let x be Element of A; :: thesis: ( ( for y being Element of A st x =~ y holds

x = y ) implies ((eqSumOf f) * (proj A)) . x = f . x )

assume A1: for y being Element of A st x =~ y holds

x = y ; :: thesis: ((eqSumOf f) * (proj A)) . x = f . x

per cases
( A is empty or not A is empty )
;

end;

suppose A2:
not A is empty
; :: thesis: ((eqSumOf f) * (proj A)) . x = f . x

then reconsider X = (proj A) . x as Element of (QuotientOrder A) by FUNCT_2:5;

A3: X in the carrier of (QuotientOrder A) by A2, SUBSET_1:def 1;

A4: x in the carrier of A by A2, SUBSET_1:def 1;

A5: X = Class ((EqRelOf A),x) by Def8;

for y being object holds

( y in X iff y = x )

A8: x in dom (proj A) by A4, A2, FUNCT_2:def 1;

A9: x in dom f by A4, FUNCT_2:def 1;

end;A3: X in the carrier of (QuotientOrder A) by A2, SUBSET_1:def 1;

A4: x in the carrier of A by A2, SUBSET_1:def 1;

A5: X = Class ((EqRelOf A),x) by Def8;

for y being object holds

( y in X iff y = x )

proof

then A7:
X = {x}
by TARSKI:def 1;
let y be object ; :: thesis: ( y in X iff y = x )

end;hereby :: thesis: ( y = x implies y in X )

thus
( y = x implies y in X )
by A4, A5, EQREL_1:20; :: thesis: verumassume A6:
y in X
; :: thesis: y = x

then y in (EqRelOf A) .: {x} by A5, RELAT_1:def 16;

then reconsider z = y as Element of A ;

[x,z] in EqRelOf A by A5, A6, EQREL_1:18;

then ( x <= z & z <= x ) by Def6;

hence y = x by A1, Def3; :: thesis: verum

end;then y in (EqRelOf A) .: {x} by A5, RELAT_1:def 16;

then reconsider z = y as Element of A ;

[x,z] in EqRelOf A by A5, A6, EQREL_1:18;

then ( x <= z & z <= x ) by Def6;

hence y = x by A1, Def3; :: thesis: verum

A8: x in dom (proj A) by A4, A2, FUNCT_2:def 1;

A9: x in dom f by A4, FUNCT_2:def 1;

per cases
( x in support f or not x in support f )
;

end;

suppose
x in support f
; :: thesis: ((eqSumOf f) * (proj A)) . x = f . x

then
eqSupport (f,X) = {x}
by A7, ZFMISC_1:46;

then canFS (eqSupport (f,X)) = <*x*> by FINSEQ_1:94;

then f * (canFS (eqSupport (f,X))) = <*(f . x)*> by A9, FINSEQ_2:34;

then Sum (f * (canFS (eqSupport (f,X)))) = f . x by RVSUM_1:73;

then (eqSumOf f) . X = f . x by A3, Def16;

hence ((eqSumOf f) * (proj A)) . x = f . x by A8, FUNCT_1:13; :: thesis: verum

end;then canFS (eqSupport (f,X)) = <*x*> by FINSEQ_1:94;

then f * (canFS (eqSupport (f,X))) = <*(f . x)*> by A9, FINSEQ_2:34;

then Sum (f * (canFS (eqSupport (f,X)))) = f . x by RVSUM_1:73;

then (eqSumOf f) . X = f . x by A3, Def16;

hence ((eqSumOf f) * (proj A)) . x = f . x by A8, FUNCT_1:13; :: thesis: verum

suppose A10:
not x in support f
; :: thesis: ((eqSumOf f) * (proj A)) . x = f . x

then
not x in eqSupport (f,X)
by XBOOLE_0:def 4;

then {x} <> eqSupport (f,X) by TARSKI:def 1;

then eqSupport (f,X) = {} by A7, XBOOLE_1:17, ZFMISC_1:33;

then Sum (f * (canFS (eqSupport (f,X)))) = 0 by RVSUM_1:72;

then (eqSumOf f) . X = 0 by A3, Def16;

then (eqSumOf f) . ((proj A) . x) = f . x by A10, PRE_POLY:def 7;

hence ((eqSumOf f) * (proj A)) . x = f . x by A8, FUNCT_1:13; :: thesis: verum

end;then {x} <> eqSupport (f,X) by TARSKI:def 1;

then eqSupport (f,X) = {} by A7, XBOOLE_1:17, ZFMISC_1:33;

then Sum (f * (canFS (eqSupport (f,X)))) = 0 by RVSUM_1:72;

then (eqSumOf f) . X = 0 by A3, Def16;

then (eqSumOf f) . ((proj A) . x) = f . x by A10, PRE_POLY:def 7;

hence ((eqSumOf f) * (proj A)) . x = f . x by A8, FUNCT_1:13; :: thesis: verum