A1: rng (L | A) c= rng L by RELAT_1:70;
( A c= dom L implies dom (L | A) = A ) by RELAT_1:62;
hence ( L | A is rng L -valued & L | A is T-Sequence-like ) by A1, Def7, RELAT_1:68, RELAT_1:def 19; :: thesis: verum