theorem :: ORDINAL4:40

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