let n, m be Element of NAT ; :: thesis: card (n * m) = (card n) *` (card m)
thus card (n * m) = card (n *^ m) by Th50
.= (card n) *` (card m) by Th25 ; :: thesis: verum