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