let f be Function of NAT ,NAT ; :: thesis: for F being Function of NAT ,REAL
for J being finite Subset of NAT st f = F & ex k being natural number st J c= Seg k holds
Sum (f | J) = Sum (Func_Seq F,(Sgm J))
let F be Function of NAT ,REAL ; :: thesis: for J being finite Subset of NAT st f = F & ex k being natural number st J c= Seg k holds
Sum (f | J) = Sum (Func_Seq F,(Sgm J))
let J be finite Subset of NAT ; :: thesis: ( f = F & ex k being natural number st J c= Seg k implies Sum (f | J) = Sum (Func_Seq F,(Sgm J)) )
assume A1: f = F ; :: thesis: ( for k being natural number holds not J c= Seg k or Sum (f | J) = Sum (Func_Seq F,(Sgm J)) )
reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;
assume A2: ex k being natural number st J c= Seg k ; :: thesis: Sum (f | J) = Sum (Func_Seq F,(Sgm J))
reconsider f9 = f | J9 as bag of J ;
A3: dom f = NAT by FUNCT_2:def 1;
then A4: J = dom (f | J9) by RELAT_1:91;
then support f9 c= J9 by PRE_POLY:37;
then consider fs being FinSequence of REAL such that
A5: fs = f9 * (canFS J9) and
A6: Sum f9 = Sum fs by UPROOTS:16;
A7: rng (canFS J) = J by FUNCT_2:def 3
.= dom f9 by A3, RELAT_1:91 ;
then dom (canFS J) = dom fs by A5, RELAT_1:46;
then A8: fs,f9 are_fiberwise_equipotent by A5, A7, CLASSES1:85;

per cases ( J is empty or not J is empty ) ;

suppose A9: J is empty ; :: thesis: Sum (f | J) = Sum (Func_Seq F,(Sgm J))

then Sgm J = {} by A2, FINSEQ_1:72;
then A10: F * (Sgm J) = {} ;
Sum fs = 0 by A5, A9, RVSUM_1:102;
hence Sum (f | J) = Sum (Func_Seq F,(Sgm J)) by A6, A10, BHSP_5:def 4, RVSUM_1:102; :: thesis: verum

end;

suppose not J is empty ; :: thesis: Sum (f | J) = Sum (Func_Seq F,(Sgm J))

then reconsider J99 = J as non empty natural-membered right_end set ;
A11: Sgm J is one-to-one by A2, FINSEQ_3:99;
rng (Sgm J) = J by A2, FINSEQ_1:def 13;
then A12: f * (Sgm J) = f * (J | (Sgm J)) by RELAT_1:125
.= (f | J) * (Sgm J) by MONOID_1:2 ;
A13: rng (Sgm J) = dom (f | J) by A2, A4, FINSEQ_1:def 13;
then dom (Sgm J) = dom ((f | J) * (Sgm J)) by RELAT_1:46;
then (f | J) * (Sgm J),f | J are_fiberwise_equipotent by A13, A11, CLASSES1:85;
then Func_Seq F,(Sgm J),f | J are_fiberwise_equipotent by A1, A12, BHSP_5:def 4;
hence Sum (f | J) = Sum (Func_Seq F,(Sgm J)) by A6, A8, CLASSES1:84, RFINSEQ:22; :: thesis: verum

end;

end;