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