theorem Th12: :: GLIBPRE1:12

for M, N being Cardinal
for f being Function st M c= card (dom f) & ( for x being object st x in dom f holds
N c= card (f . x) ) holds
M *` N c= Sum (Card f)