theorem Th48: :: INT_5:48

for X being finite set
for f being FinSequence of bool X st ( for d, e being Nat st d in dom f & e in dom f & d <> e holds
f . d misses f . e ) holds
card (union (rng f)) = Sum (Card f)