( Sq_Circ is Function of (TOP-REAL 2),(TOP-REAL 2) & rng Sq_Circ = the carrier of (TOP-REAL 2) & ( for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds
f is being_homeomorphism ) )