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 Sequence-like ) by A1, RELAT_1:68; :: thesis: verum