let f be sequence of NAT; :: thesis: for F being sequence of REAL
for J being included_in_Seg Subset of NAT st f = F holds
Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))
let F be sequence of REAL; :: thesis: for J being included_in_Seg Subset of NAT st f = F holds
Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))
let J be included_in_Seg Subset of NAT; :: thesis: ( f = F implies Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) )
assume A1: f = F ; :: thesis: Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))
reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;
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:62;
support f9 c= J9 ;
then consider fs being FinSequence of REAL such that
A5: fs = f9 * (canFS J9) and
A6: Sum f9 = Sum fs by UPROOTS:14;
A7: rng (canFS J) = J by FUNCT_2:def 3
.= dom f9 by A3, RELAT_1:62 ;
then dom (canFS J) = dom fs by A5, RELAT_1:27;
then A8: fs,f9 are_fiberwise_equipotent by A5, A7, CLASSES1:77;
A9: Sgm J is one-to-one by FINSEQ_3:92;
rng (Sgm J) = J by FINSEQ_1:def 14;
then A10: f * (Sgm J) = f * (J |` (Sgm J))
.= (f | J) * (Sgm J) by MONOID_1:1 ;
A11: rng (Sgm J) = dom (f | J) by A4, FINSEQ_1:def 14;
then dom (Sgm J) = dom ((f | J) * (Sgm J)) by RELAT_1:27;
then (f | J) * (Sgm J),f | J are_fiberwise_equipotent by A11, A9, CLASSES1:77;
then Func_Seq (F,(Sgm J)),f | J are_fiberwise_equipotent by A1, A10, BHSP_5:def 4;
hence Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) by A6, A8, CLASSES1:76, RFINSEQ:9; :: thesis: verum