let I, j be set ; :: thesis: for f being Function of I, NAT
for J being finite Subset of st J = {j} holds
Sum (f | J) = f . j
let f be Function of I, NAT ; :: thesis: for J being finite Subset of st J = {j} holds
Sum (f | J) = f . j
let J be finite Subset of ; :: thesis: ( J = {j} implies Sum (f | J) = f . j )
consider f' being FinSequence of REAL such that
A1: Sum (f | J) = Sum f' and
A2: f' = (f | J) * (canFS (support (f | J))) by UPROOTS:def 3;
assume A3: J = {j} ; :: thesis: Sum (f | J) = f . j
then A4: j in J by TARSKI:def 1;
then j in I ;
then j in dom f by FUNCT_2:def 1;
then J c= dom f by A3, ZFMISC_1:37;
then A5: dom (f | J) = J by RELAT_1:91;
then A6: support (f | J) c= J by PRE_POLY:37;

per cases ( support (f | J) = {} or support (f | J) = J ) by A3, A6, ZFMISC_1:39;

suppose A7: support (f | J) = {} ; :: thesis: Sum (f | J) = f . j

now

assume f . j <> 0 ; :: thesis: contradiction
then (f | J) . j <> 0 by A4, FUNCT_1:72;
hence contradiction by A7, PRE_POLY:def 7; :: thesis: verum

end;

hence Sum (f | J) = f . j by A1, A2, A7, RVSUM_1:102; :: thesis: verum

end;

suppose support (f | J) = J ; :: thesis: Sum (f | J) = f . j

then canFS (support (f | J)) = <*j*> by A3, UPROOTS:6;
then f' = <*((f | J) . j)*> by A4, A5, A2, BAGORDER:3;
then f' = <*(f . j)*> by A4, FUNCT_1:72;
hence Sum (f | J) = f . j by A1, RVSUM_1:103; :: thesis: verum

end;

end;