let a be Ordinal; a +^ a = 2 *^ a
consider fi being Ordinal-Sequence such that
A1:
( 2 *^ a = last fi & dom fi = succ 2 & fi . 0 = 0 )
and
A2:
for c being Ordinal st succ c in succ 2 holds
fi . (succ c) = (fi . c) +^ a
and
for c being Ordinal st c in succ 2 & c <> 0 & c is limit_ordinal holds
fi . c = union (sup (fi | c))
by ORDINAL2:def 15;
( succ 0 in succ (succ 0) & succ (succ 0) in succ 2 )
by ORDINAL1:6;
then A3:
( succ 0 in succ 2 & succ (succ 0) in succ 2 )
by ORDINAL1:10;
2 *^ a =
fi . 2
by A1, ORDINAL2:6
.=
(fi . (succ 0)) +^ a
by A2, A3
.=
((fi . 0) +^ a) +^ a
by A2, A3
.=
a +^ a
by A1, ORDINAL2:30
;
hence
a +^ a = 2 *^ a
; verum