let B, A be Ordinal; :: thesis: ( B <> {} implies union (A +^ B) = A +^ (union B) )
assume A1: B <> {} ; :: thesis: union (A +^ B) = A +^ (union B)

A2: now

given C being Ordinal such that A3: B = succ C ; :: thesis: union (A +^ B) = A +^ (union B)
thus union (A +^ B) = union (succ (A +^ C)) by A3, ORDINAL2:45
.= A +^ C by ORDINAL2:2
.= A +^ (union B) by A3, ORDINAL2:2 ; :: thesis: verum

end;

now

assume for C being Ordinal holds not B = succ C ; :: thesis: union (A +^ B) = A +^ (union B)
then A4: B is limit_ordinal by ORDINAL1:42;
then A +^ B is limit_ordinal by A1, Th32;
then ( union (A +^ B) = A +^ B & union B = B ) by A4, ORDINAL1:def 6;
hence union (A +^ B) = A +^ (union B) ; :: thesis: verum

end;

hence union (A +^ B) = A +^ (union B) by A2; :: thesis: verum