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 13;
A3: dom f = I by FUNCT_2:def 1;
support f9 c= J9 ;
then consider fs being FinSequence of REAL such that
A4: fs = f9 * (canFS J9) and
A5: Sum f9 = Sum fs by UPROOTS:14;
A6: rng (canFS J) = J by FUNCT_2:def 3
.= dom f9 by A3, RELAT_1:62 ;
then dom (canFS J) = dom fs by A4, RELAT_1:27;
then fs,f9 are_fiberwise_equipotent by A4, A6, CLASSES1:77;
then Sum fs = Sum (FinS (F,J)) by A2, CLASSES1:76, RFINSEQ:9;
hence Sum (f | J) = Sum (F,J) by A5, RFUNCT_3:def 14; :: thesis: verum