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;

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;

end;

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

end;

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

hence
Sum (f | J) = f . j
by A1, A2, A6, RVSUM_1:72; :: thesis: verumassume
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;then (f | J) . j <> 0 by A4, FUNCT_1:49;

hence contradiction by A6, PRE_POLY:def 7; :: thesis: verum