theorem Th23: :: REVROT_1:23
for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds
rng (Y_axis f) = rng (Y_axis g) by Th22;