let p, q be Sequence; :: thesis: dom p c= dom (p ^ q)
dom (p ^ q) = (dom p) +^ (dom q) by ORDINAL4:def 1;
hence dom p c= dom (p ^ q) by ORDINAL3:24; :: thesis: verum