scheme :: MSAFREE5:sch 1
CardUnion{ F₁( object ) -> set , F₂() -> FinSequence of NAT } :

card (union { F₁(i) where i is Nat : i < len F₂() } ) = Sum F₂()

provided

A1: for i, j being Nat st i < len F₂() & j < len F₂() & i <> j holds
F₁(i) misses F₁(j) and
A2: for i being Nat st i < len F₂() holds
card F₁(i) = F₂() . (i + 1)