dom (O --> x) = O by FUNCOP_1:19;
hence O --> x is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum