let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( rng f = rng g implies rng (Y_axis f) = rng (Y_axis g) )
assume rng f = rng g ; :: thesis: rng (Y_axis f) = rng (Y_axis g)
hence ( rng (Y_axis f) c= rng (Y_axis g) & rng (Y_axis g) c= rng (Y_axis f) ) by Th22; :: according to XBOOLE_0:def 10 :: thesis: verum