for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds
rng (X_axis f) = rng (X_axis g) by Th20;