theorem Th55: :: FINSEQ_3:57

for p, q being FinSequence
for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))