let f be sequence of NAT; :: thesis: for F being sequence of REAL

for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds

Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))

let F be sequence of REAL; :: thesis: for J being finite Subset of NAT st f = F & ex k being Nat 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 Nat st J c= Seg k implies Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) )

assume A1: f = F ; :: thesis: ( for k being Nat 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 Nat 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: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 A2, FINSEQ_3:92;

rng (Sgm J) = J by A2, FINSEQ_1:def 13;

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 A2, A4, FINSEQ_1:def 13;

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

for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds

Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))

let F be sequence of REAL; :: thesis: for J being finite Subset of NAT st f = F & ex k being Nat 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 Nat st J c= Seg k implies Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) )

assume A1: f = F ; :: thesis: ( for k being Nat 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 Nat 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: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 A2, FINSEQ_3:92;

rng (Sgm J) = J by A2, FINSEQ_1:def 13;

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 A2, A4, FINSEQ_1:def 13;

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