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