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