(* begin hide *)
(* In this file a notion of morphism between two arbitrary real number
structures, is introduced together with te proofs that this notion of
morphism preserves the basic algebraic structure. *)
(* begin hide *)
(* In this file a notion of morphism between two arbitrary real number
structures, is introduced together with te proofs that this notion of
morphism preserves the basic algebraic structure. *)