for f, h being natural-valued FinSequence st ( for i being Nat holds card (Coim (h,i)) = f . i ) holds
Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...)