let k, n be Nat; :: thesis: ( n * k = n *` k & n + k = n +` k )
A1: k = card k ;
n = card n ;
then ( n *` k = card (n * k) & n +` k = card (n + k) ) by A1, CARD_2:39, CARD_2:38;
hence ( n * k = n *` k & n + k = n +` k ) ; :: thesis: verum