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

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

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

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

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 )

proof

let y be object ; :: thesis: ( y in X iff y = x )

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

assume 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;

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

end;

then A7: X = {x} by TARSKI:def 1;
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 ) ;

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;

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;

end;

end;

end;