for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A