let I be non empty set ; 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; 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; for J being finite Subset of I st f = F holds
Sum (f | J) = Sum (F,J)
let J be finite Subset of I; ( 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
; 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; verum