let I, j be set ; :: thesis: for f being Function of I,NAT
for J being finite Subset of I st J = {j} holds
Sum (f | J) = f . j
let f be Function of I,NAT ; :: thesis: for J being finite Subset of I st J = {j} holds
Sum (f | J) = f . j
let J be finite Subset of I; :: thesis: ( J = {j} implies Sum (f | J) = f . j )
assume A1: J = {j} ; :: thesis: Sum (f | J) = f . j
then A2: 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 A1, ZFMISC_1:37;
then A3: dom (f | J) = J by RELAT_1:91;
then A4: support (f | J) c= J by POLYNOM1:41;
consider f' being FinSequence of REAL such that
A5: ( Sum (f | J) = Sum f' & f' = (f | J) * (canFS (support (f | J))) ) by UPROOTS:def 3;

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

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

now

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

end;

hence Sum (f | J) = f . j by A6, A5, RVSUM_1:102; :: thesis: verum

end;

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

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

end;

end;