let I be non empty set ; :: thesis: for F being PartFunc of I,REAL
for f being Function of I,NAT
for J being finite Subset of I st f = F holds
Sum (f | J) = Sum F,J
let F be PartFunc of I,REAL ; :: thesis: for f being Function of I,NAT
for J being finite Subset of I st f = F holds
Sum (f | J) = Sum F,J
let f be Function of I,NAT ; :: thesis: for J being finite Subset of I st f = F holds
Sum (f | J) = Sum F,J
let J be finite Subset of I; :: thesis: ( f = F implies Sum (f | J) = Sum F,J )
reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;
reconsider f9 = f | J9 as bag of J ;
A1: dom (F | J) is finite ;
assume f = F ; :: thesis: Sum (f | J) = Sum F,J
then A2: f | J, FinS F,J are_fiberwise_equipotent by A1, RFUNCT_3:def 14;
A3: dom f = I by FUNCT_2:def 1;
then J = dom (f | J9) by RELAT_1:91;
then support f9 c= J9 by PRE_POLY:37;
then consider fs being FinSequence of REAL such that
A4: fs = f9 * (canFS J9) and
A5: Sum f9 = Sum fs by UPROOTS:16;
A6: rng (canFS J) = J by FUNCT_2:def 3
.= dom f9 by A3, RELAT_1:91 ;
then dom (canFS J) = dom fs by A4, RELAT_1:46;
then fs,f9 are_fiberwise_equipotent by A4, A6, CLASSES1:85;
then Sum fs = Sum (FinS F,J) by A2, CLASSES1:84, RFINSEQ:22;
hence Sum (f | J) = Sum F,J by A5, RFUNCT_3:def 15; :: thesis: verum