let n, m be Element of NAT ; :: thesis: card (n + m) = (card n) +` (card m)
thus card (n + m) = card (n +^ m) by Th49
.= (card n) +` (card m) by Th24 ; :: thesis: verum