let n, m be Nat; :: thesis: ( n +` m = n + m & n *` m = n * m )
thus n +` m = (card n) +` (card m)
.= card (n + m) by CARD_2:38
.= n + m ; :: thesis: n *` m = n * m
thus n *` m = card [:n,m:] by CARD_2:def 2
.= (card n) * (card m) by CARD_2:46
.= n * m ; :: thesis: verum