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