let a, b be Ordinal; :: thesis: ( ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) implies a (+) b = a +^ b )
assume A1: ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) ; :: thesis: a (+) b = a +^ b

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose a = 0 ; :: thesis: a (+) b = a +^ b

then ( a (+) b = b & a +^ b = b ) by Th82, ORDINAL2:30;
hence a (+) b = a +^ b ; :: thesis: verum

end;

suppose b = 0 ; :: thesis: a (+) b = a +^ b

then ( a (+) b = a & a +^ b = a ) by Th82, ORDINAL2:27;
hence a (+) b = a +^ b ; :: thesis: verum

end;

suppose A2: ( a <> 0 & b <> 0 ) ; :: thesis: a (+) b = a +^ b

then omega -exponent (Sum^ (CantorNF b)) in omega -exponent (last (CantorNF a)) by A1;
then omega -exponent ((CantorNF b) . 0) in omega -exponent (last (CantorNF a)) by Th44;
then A3: (CantorNF a) ^ (CantorNF b) is Cantor-normal-form by A2, Th33;
thus a (+) b = (Sum^ (CantorNF a)) (+) (Sum^ (CantorNF b))
.= a +^ b by A3, Th84 ; :: thesis: verum

end;

end;