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;
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