let n, m be Nat; :: thesis: n (+) m = n + m
thus n (+) m = n +^ m by Th88
.= n + m by CARD_2:36 ; :: thesis: verum