for A, B being Sequence holds Card (A ^ B) = (Card A) ^ (Card B)