theorem :: NUMBER19:15

for f, g being XFinSequence
for X being set holds card ((f ^ g) " X) = (card (f " X)) + (card (g " X))