dom (k --> x) = k by FUNCOP_1:19;
then dom (k --> x) is ordinal ;
hence for b₁ being Function st b₁ = k --> x holds
b₁ is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum