for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G