let I be set ; :: thesis: for f being Function of I,NAT
for J being finite Subset of I
for j being object st J = {j} holds
Sum (f | J) = f . j
let f be Function of I,NAT; :: thesis: for J being finite Subset of I
for j being object st J = {j} holds
Sum (f | J) = f . j
let J be finite Subset of I; :: thesis: for j being object st J = {j} holds
Sum (f | J) = f . j
let j be object ; :: thesis: ( J = {j} implies Sum (f | J) = f . j )
consider f9 being FinSequence of REAL such that
A1: Sum (f | J) = Sum f9 and
A2: f9 = (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:31;
then A5: dom (f | J) = J by RELAT_1:62;

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

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

now :: thesis: not f . j <> 0

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

end;

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

end;

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

then canFS (support (f | J)) = <*j*> by A3, FINSEQ_1:94;
then f9 = <*((f | J) . j)*> by A4, A5, A2, FINSEQ_2:34;
then f9 = <*(f . j)*> by A4, FUNCT_1:49;
hence Sum (f | J) = f . j by A1, RVSUM_1:73; :: thesis: verum

end;

end;