for A, B being Sequence holds rng A c= rng (A ^ B) by Th7A;