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

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