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