theorem :: STIRL2_1:66

for D being non empty set
for F being XFinSequence of D st ( for i being Nat st i in dom F holds
F . i is finite ) & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) holds
ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF ) by Lm2;