theorem :: ORDINAL4:39

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