theorem Th24: :: PRE_POLY:25

for F, G being FinSequence holds Card (F ^ G) = (Card F) ^ (Card G)