for A, B being finite Ordinal-Sequence st dom A c= dom B & ( for a being object st a in dom A holds
A . a c= B . a ) holds
Sum^ A c= Sum^ B