let X be set ; :: thesis: for S being Sequence st dom S = NAT holds
last S = S . NAT
let S be Sequence; :: thesis: ( dom S = NAT implies last S = S . NAT )
assume dom S = NAT ; :: thesis: last S = S . NAT
then union (dom S) = NAT by ORDINAL1:def 6;
hence last S = S . NAT by ORDINAL2:def 1; :: thesis: verum