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 J' = J as finite Subset of J by ZFMISC_1:def 1;
reconsider f' = f | J' as bag of ;
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 | J') by RELAT_1:91;
then support f' c= J' by PRE_POLY:37;
then consider fs being FinSequence of REAL such that
A4: fs = f' * (canFS J') and
A5: Sum f' = Sum fs by UPROOTS:16;
A6: rng (canFS J) = J by FUNCT_2:def 3
.= dom f' by A3, RELAT_1:91 ;
then dom (canFS J) = dom fs by A4, RELAT_1:46;
then fs,f' 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