( dom (p (#) q) = (dom p) /\ (dom q) & dom p is ordinal & dom q is ordinal ) by VALUED_1:def 4;
hence p (#) q is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum