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 )
assume A1: f = F ; :: thesis: Sum (f | J) = Sum F,J
reconsider J' = J as finite Subset of J by ZFMISC_1:def 1;
A2: dom f = I by FUNCT_2:def 1;
then A3: J = dom (f | J') by RELAT_1:91;
reconsider f' = f | J' as bag of ;
support f' c= J' by A3, POLYNOM1:41;
then consider fs being FinSequence of REAL such that
A4: ( fs = f' * (canFS J') & Sum f' = Sum fs ) by UPROOTS:16;
dom (F | J) is finite ;
then A5: f | J, FinS F,J are_fiberwise_equipotent by A1, RFUNCT_3:def 14;
A6: rng (canFS J) = J by FUNCT_2:def 3
.= dom f' by A2, RELAT_1:91 ;
then A7: dom (canFS J) = dom fs by A4, RELAT_1:46;
fs,f' are_fiberwise_equipotent by A4, A7, A6, CLASSES1:85;
then Sum fs = Sum (FinS F,J) by RFINSEQ:22, A5, CLASSES1:84;
hence Sum (f | J) = Sum F,J by A4, RFUNCT_3:def 15; :: thesis: verum