let A be Ordinal; :: thesis: A +^ 1 = succ A
thus A +^ 1 = succ (A +^ {}) by Lm1, Th45
.= succ A by Th44 ; :: thesis: verum