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

A2: now :: thesis: ( ( for C being Ordinal holds not B = succ C ) implies union (A +^ B) = A +^ (union B) )

assume for C being Ordinal holds not B = succ C ; :: thesis: union (A +^ B) = A +^ (union B)
then A3: B is limit_ordinal by ORDINAL1:29;
then A +^ B is limit_ordinal by A1, Th29;
then union (A +^ B) = A +^ B ;
hence union (A +^ B) = A +^ (union B) by A3; :: thesis: verum

end;

now :: thesis: ( ex C being Ordinal st B = succ C implies union (A +^ B) = A +^ (union B) )

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

end;

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