:: by Krzysztof Hryniewiecki

::

:: Received January 8, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

registration

cluster -> real Element of REAL ;

coherence

for b_{1} being Element of REAL holds b_{1} is real

end;
coherence

for b

proof end;

registration

cluster V11() ext-real positive real Element of REAL ;

existence

ex b_{1} being Real st b_{1} is positive

end;
existence

ex b

proof end;

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;