for n, m being Nat holds
( n +` m = n + m & n *` m = n * m )