A1: rng (L | A) c= rng L by RELAT_1:99;
( A c= dom L implies dom (L | A) = A ) by RELAT_1:91;
hence L | A is T-Sequence of rng L by A1, Def7, RELAT_1:97, RELAT_1:def 19; :: thesis: verum