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
(() * (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
(() * (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 (() * (proj A)) . x = f . x )

assume A1: for y being Element of A st x =~ y holds
x = y ; :: thesis: (() * (proj A)) . x = f . x
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: (() * (proj A)) . x = f . x
hence ((eqSumOf f) * (proj A)) . x = f . x ; :: thesis: verum
end;
suppose A2: not A is empty ; :: thesis: (() * (proj A)) . x = f . x
then reconsider X = (proj A) . x as Element of () by FUNCT_2:5;
A3: X in the carrier of () by ;
A4: x in the carrier of A by ;
A5: X = Class ((),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 () .: {x} by ;
then reconsider z = y as Element of A ;
[x,z] in EqRelOf A by ;
then ( x <= z & z <= x ) by Def6;
hence y = x by ; :: thesis: verum
end;
thus ( y = x implies y in X ) by ; :: thesis: verum
end;
then A7: X = {x} by TARSKI:def 1;
A8: x in dom (proj A) by ;
A9: x in dom f by ;
per cases ( x in support f or not x in support f ) ;
suppose x in support f ; :: thesis: (() * (proj A)) . x = f . x
then eqSupport (f,X) = {x} by ;
then canFS (eqSupport (f,X)) = <*x*> by FINSEQ_1:94;
then f * (canFS (eqSupport (f,X))) = <*(f . x)*> by ;
then Sum (f * (canFS (eqSupport (f,X)))) = f . x by RVSUM_1:73;
then (eqSumOf f) . X = f . x by ;
hence ((eqSumOf f) * (proj A)) . x = f . x by ; :: thesis: verum
end;
suppose A10: not x in support f ; :: thesis: (() * (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 ;
then Sum (f * (canFS (eqSupport (f,X)))) = 0 by RVSUM_1:72;
then (eqSumOf f) . X = 0 by ;
then (eqSumOf f) . ((proj A) . x) = f . x by ;
hence ((eqSumOf f) * (proj A)) . x = f . x by ; :: thesis: verum
end;
end;
end;
end;