let F be Cardinal-Function; :: thesis: card (Union F) c= Sum F
Card F = F by Th1;
hence card (Union F) c= Sum F by Th39; :: thesis: verum