[STATEMENT]
lemma cardinalityPreservation: 
  assumes "\<forall>X \<in> XX. finite X" "is_non_overlapping XX" 
  shows   "card (\<Union> XX) = sum card XX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union> XX) = sum card XX
[PROOF STEP]
by (metis assms is_non_overlapping_def card_Union_disjoint disjointI)