theorem Th14: :: GLIBPRE1:14
for X being set st X is mutually-disjoint holds
Sum (Card (id X)) = card (union X)