let m, n be Nat; :: thesis: card (n * m) = (card n) *` (card m)
thus card (n * m) = card (n *^ m) by Th36
.= (card n) *` (card m) by Th13 ; :: thesis: verum