let x be set ; :: thesis: last <%x%> = x
dom <%x%> = succ 0 by AFINSQ_1:def 4;
then union (dom <%x%>) = 0 by ORDINAL2:2;
hence last <%x%> = x ; :: thesis: verum