theorem :: GLIBPRE1:15

for X being set
for M, N being Cardinal st X is mutually-disjoint & M c= card X & ( for Y being set st Y in X holds
N c= card Y ) holds
M *` N c= card (union X)