:: by Krzysztof Hryniewiecki

::

:: Received January 8, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let x be Real;

:: original: -

redefine func - x -> Real;

coherence

- x is Real by XREAL_0:def 1;

:: original: "

redefine func x " -> Real;

coherence

x " is Real by XREAL_0:def 1;

end;
:: original: -

redefine func - x -> Real;

coherence

- x is Real by XREAL_0:def 1;

:: original: "

redefine func x " -> Real;

coherence

x " is Real by XREAL_0:def 1;

definition

let x be real number ;

let y be Real;

:: original: +

redefine func x + y -> Real;

coherence

x + y is Real by XREAL_0:def 1;

:: original: *

redefine func x * y -> Real;

coherence

x * y is Real by XREAL_0:def 1;

:: original: -

redefine func x - y -> Real;

coherence

x - y is Real by XREAL_0:def 1;

:: original: /

redefine func x / y -> Real;

coherence

x / y is Real by XREAL_0:def 1;

end;
let y be Real;

:: original: +

redefine func x + y -> Real;

coherence

x + y is Real by XREAL_0:def 1;

:: original: *

redefine func x * y -> Real;

coherence

x * y is Real by XREAL_0:def 1;

:: original: -

redefine func x - y -> Real;

coherence

x - y is Real by XREAL_0:def 1;

:: original: /

redefine func x / y -> Real;

coherence

x / y is Real by XREAL_0:def 1;

definition

let x be Real;

let y be real number ;

:: original: +

redefine func x + y -> Real;

coherence

x + y is Real by XREAL_0:def 1;

:: original: *

redefine func x * y -> Real;

coherence

x * y is Real by XREAL_0:def 1;

:: original: -

redefine func x - y -> Real;

coherence

x - y is Real by XREAL_0:def 1;

:: original: /

redefine func x / y -> Real;

coherence

x / y is Real by XREAL_0:def 1;

end;
let y be real number ;

:: original: +

redefine func x + y -> Real;

coherence

x + y is Real by XREAL_0:def 1;

:: original: *

redefine func x * y -> Real;

coherence

x * y is Real by XREAL_0:def 1;

:: original: -

redefine func x - y -> Real;

coherence

x - y is Real by XREAL_0:def 1;

:: original: /

redefine func x / y -> Real;

coherence

x / y is Real by XREAL_0:def 1;