:: by Andrzej Trybulec

::

:: Received January 9, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

Lm1: for x being Element of REAL+ holds [0,x] in [:{0},REAL+:]

proof end;

Lm2: for a, b being set holds not 1 = [a,b]

proof end;

Lm3: 0 in REAL

by NUMBERS:19;

definition

let x, y be Element of REAL ;

( ( x in REAL+ & y in REAL+ implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = [0,(x9 + y9)] ) ) )

for b_{1}, b_{2} being Element of REAL holds

( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 + y9 ) & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{2} = x9 + y9 ) implies b_{1} = b_{2} ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = x9 - y9 ) & ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{2} = x9 - y9 ) implies b_{1} = b_{2} ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = y9 - x9 ) & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{2} = y9 - x9 ) implies b_{1} = b_{2} ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{2} = [0,(x9 + y9)] ) implies b_{1} = b_{2} ) )

for b_{1} being Element of REAL holds

( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = x9 - y9 ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = y9 - x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = x9 - y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = y9 - x9 ) ) ) )
by Th5, XBOOLE_0:3;

commutativity

for b_{1}, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = [0,(x9 + y9)] ) ) holds

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & b_{1} = x9 + y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = [0,y9] & b_{1} = x9 - y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = y9 & b_{1} = y9 - x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & b_{1} = [0,(x9 + y9)] ) ) )
;

( ( x in REAL+ & y in REAL+ implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b_{1} being Element of REAL ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b_{1} being Element of REAL st b_{1} = 0 ) )

for b_{1}, b_{2} being Element of REAL holds

( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{2} = x9 *' y9 ) implies b_{1} = b_{2} ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{2} = [0,(x9 *' y9)] ) implies b_{1} = b_{2} ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{2} = [0,(y9 *' x9)] ) implies b_{1} = b_{2} ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{2} = y9 *' x9 ) implies b_{1} = b_{2} ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Element of REAL holds

( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) ) ) )
by Th5, XBOOLE_0:3;

commutativity

for b_{1}, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{1} = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{1} = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{1} = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{1} = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies b_{1} = 0 ) holds

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & b_{1} = x9 *' y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = [0,y9] & b_{1} = [0,(x9 *' y9)] ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = y9 & b_{1} = [0,(y9 *' x9)] ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & b_{1} = y9 *' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) implies b_{1} = 0 ) )
;

end;
func + (x,y) -> Element of REAL means :Def1: :: ARYTM_0:def 1

ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & it = x9 + y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & it = x9 - y9 ) if ( x in REAL+ & y in [:{0},REAL+:] )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & it = y9 - x9 ) if ( y in REAL+ & x in [:{0},REAL+:] )

otherwise ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & it = [0,(x9 + y9)] );

existence ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & it = x9 + y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & it = x9 - y9 ) if ( x in REAL+ & y in [:{0},REAL+:] )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & it = y9 - x9 ) if ( y in REAL+ & x in [:{0},REAL+:] )

otherwise ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & it = [0,(x9 + y9)] );

( ( x in REAL+ & y in REAL+ implies ex b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

proof end;

uniqueness for b

( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

( x = [0,x9] & y = [0,y9] & b

proof end;

consistency for b

( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = x9 & y = y9 & b

( x = [0,x9] & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

commutativity

for b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & b

( y = x9 & x = [0,y9] & b

( y = [0,x9] & x = y9 & b

( y = [0,x9] & x = [0,y9] & b

func * (x,y) -> Element of REAL means :Def2: :: ARYTM_0:def 2

ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & it = x9 *' y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & it = [0,(x9 *' y9)] ) if ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & it = [0,(y9 *' x9)] ) if ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & it = y9 *' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )

otherwise it = 0 ;

existence ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & it = x9 *' y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & it = [0,(x9 *' y9)] ) if ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & it = [0,(y9 *' x9)] ) if ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & it = y9 *' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )

otherwise it = 0 ;

( ( x in REAL+ & y in REAL+ implies ex b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

proof end;

uniqueness for b

( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

( x = [0,x9] & y = [0,y9] & b

proof end;

consistency for b

( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = x9 & y = y9 & b

( x = [0,x9] & y = y9 & b

( x = x9 & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

commutativity

for b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & b

( y = x9 & x = [0,y9] & b

( y = [0,x9] & x = y9 & b

( y = [0,x9] & x = [0,y9] & b

:: deftheorem Def1 defines + ARYTM_0:def 1 :

for x, y, b_{3} being Element of REAL holds

( ( x in REAL+ & y in REAL+ implies ( b_{3} = + (x,y) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{3} = x9 + y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ( b_{3} = + (x,y) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{3} = x9 - y9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ( b_{3} = + (x,y) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{3} = y9 - x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ( b_{3} = + (x,y) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{3} = [0,(x9 + y9)] ) ) ) );

for x, y, b

( ( x in REAL+ & y in REAL+ implies ( b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

:: deftheorem Def2 defines * ARYTM_0:def 2 :

for x, y, b_{3} being Element of REAL holds

( ( x in REAL+ & y in REAL+ implies ( b_{3} = * (x,y) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & b_{3} = x9 *' y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( b_{3} = * (x,y) iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = [0,y9] & b_{3} = [0,(x9 *' y9)] ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( b_{3} = * (x,y) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = y9 & b_{3} = [0,(y9 *' x9)] ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( b_{3} = * (x,y) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & b_{3} = y9 *' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( b_{3} = * (x,y) iff b_{3} = 0 ) ) );

for x, y, b

( ( x in REAL+ & y in REAL+ implies ( b

( x = x9 & y = y9 & b

( x = x9 & y = [0,y9] & b

( x = [0,x9] & y = y9 & b

( x = [0,x9] & y = [0,y9] & b

reconsider jj = 1 as Element of REAL by NUMBERS:19;

definition

let x be Element of REAL ;

existence

ex b_{1} being Element of REAL st + (x,b_{1}) = 0

for b_{1}, b_{2} being Element of REAL st + (x,b_{1}) = 0 & + (x,b_{2}) = 0 holds

b_{1} = b_{2}

for b_{1}, b_{2} being Element of REAL st + (b_{2},b_{1}) = 0 holds

+ (b_{1},b_{2}) = 0
;

( ( x <> 0 implies ex b_{1} being Element of REAL st * (x,b_{1}) = 1 ) & ( not x <> 0 implies ex b_{1} being Element of REAL st b_{1} = 0 ) )

for b_{1}, b_{2} being Element of REAL holds

( ( x <> 0 & * (x,b_{1}) = 1 & * (x,b_{2}) = 1 implies b_{1} = b_{2} ) & ( not x <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Element of REAL holds verum
;

involutiveness

for b_{1}, b_{2} being Element of REAL st ( b_{2} <> 0 implies * (b_{2},b_{1}) = 1 ) & ( not b_{2} <> 0 implies b_{1} = 0 ) holds

( ( b_{1} <> 0 implies * (b_{1},b_{2}) = 1 ) & ( not b_{1} <> 0 implies b_{2} = 0 ) )

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

+ (b

func inv x -> Element of REAL means :Def4: :: ARYTM_0:def 4

* (x,it) = 1 if x <> 0

otherwise it = 0 ;

existence * (x,it) = 1 if x <> 0

otherwise it = 0 ;

( ( x <> 0 implies ex b

proof end;

uniqueness for b

( ( x <> 0 & * (x,b

proof end;

consistency for b

involutiveness

for b

( ( b

proof end;

:: deftheorem Def3 defines opp ARYTM_0:def 3 :

for x, b_{2} being Element of REAL holds

( b_{2} = opp x iff + (x,b_{2}) = 0 );

for x, b

( b

:: deftheorem Def4 defines inv ARYTM_0:def 4 :

for x, b_{2} being Element of REAL holds

( ( x <> 0 implies ( b_{2} = inv x iff * (x,b_{2}) = 1 ) ) & ( not x <> 0 implies ( b_{2} = inv x iff b_{2} = 0 ) ) );

for x, b

( ( x <> 0 implies ( b

Lm4: for x, y, z being set st [x,y] = {z} holds

( z = {x} & x = y )

proof end;

definition

let x, y be Element of REAL ;

for b_{1} being Element of COMPLEX holds verum
;

coherence

( ( y = 0 implies x is Element of COMPLEX ) & ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX ) )

end;
func [*x,y*] -> Element of COMPLEX equals :Def5: :: ARYTM_0:def 5

x if y = 0

otherwise (0,1) --> (x,y);

consistency x if y = 0

otherwise (0,1) --> (x,y);

for b

coherence

( ( y = 0 implies x is Element of COMPLEX ) & ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX ) )

proof end;

:: deftheorem Def5 defines [* ARYTM_0:def 5 :

for x, y being Element of REAL holds

( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) );

for x, y being Element of REAL holds

( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) );

set RR = [:{0},REAL+:] \ {[0,0]};

reconsider o = 0 as Element of REAL by Lm3;