:: by Krzysztof Hryniewiecki

::

:: Received January 8, 1989

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

definition

let x be Element of REAL ;

:: original: -

redefine func - x -> Element of REAL ;

coherence

- x is Element of REAL by XREAL_0:def 1;

:: original: "

redefine func x " -> Element of REAL ;

coherence

x " is Element of REAL by XREAL_0:def 1;

end;
:: original: -

redefine func - x -> Element of REAL ;

coherence

- x is Element of REAL by XREAL_0:def 1;

:: original: "

redefine func x " -> Element of REAL ;

coherence

x " is Element of REAL by XREAL_0:def 1;

definition

let x, y be Element of REAL ;

:: original: +

redefine func x + y -> Element of REAL ;

coherence

x + y is Element of REAL by XREAL_0:def 1;

:: original: *

redefine func x * y -> Element of REAL ;

coherence

x * y is Element of REAL by XREAL_0:def 1;

:: original: -

redefine func x - y -> Element of REAL ;

coherence

x - y is Element of REAL by XREAL_0:def 1;

:: original: /

redefine func x / y -> Element of REAL ;

coherence

x / y is Element of REAL by XREAL_0:def 1;

end;
:: original: +

redefine func x + y -> Element of REAL ;

coherence

x + y is Element of REAL by XREAL_0:def 1;

:: original: *

redefine func x * y -> Element of REAL ;

coherence

x * y is Element of REAL by XREAL_0:def 1;

:: original: -

redefine func x - y -> Element of REAL ;

coherence

x - y is Element of REAL by XREAL_0:def 1;

:: original: /

redefine func x / y -> Element of REAL ;

coherence

x / y is Element of REAL by XREAL_0:def 1;