:: ARYTM_0 semantic presentation

Lm1: {} in {{} }
by TARSKI:def 1;

theorem Th1: :: ARYTM_0:1
REAL+ c= REAL
proof end;

theorem Th2: :: ARYTM_0:2
for x being Element of REAL+ st x <> {} holds
[{} ,x] in REAL
proof end;

theorem Th3: :: ARYTM_0:3
for y being set st [{} ,y] in REAL holds
y <> {}
proof end;

theorem Th4: :: ARYTM_0:4
for x, y being Element of REAL+ holds x - y in REAL
proof end;

theorem Th5: :: ARYTM_0:5
REAL+ misses [:{{} },REAL+ :]
proof end;

theorem Th6: :: ARYTM_0:6
for x, y being Element of REAL+ st x - y = {} holds
x = y
proof end;

theorem Th7: :: ARYTM_0:7
for a, b being set holds not 1 = [a,b]
proof end;

theorem Th8: :: ARYTM_0:8
for x, y, z being Element of REAL+ st x <> {} & x *' y = x *' z holds
y = z
proof end;

definition
let x, y be Element of REAL ;
canceled;
func + x,y -> Element of REAL means :Def2: :: ARYTM_0:def 2
 ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' + y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & it = x' - y' ) if ( x in REAL+ & y in [:{0 },REAL+ :] )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & it = y' - x' ) if ( y in REAL+ & x in [:{0 },REAL+ :] )
otherwise ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & it = [0 ,(x' + y')] );
existence
( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) & ( ( 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 b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b2 = x' + y' ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b2 = x' - y' ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b2 = y' - x' ) implies b1 = b2 ) & ( ( 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 x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b2 = [0 ,(x' + y')] ) implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) iff ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] & y in REAL+ & x in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) ) ) by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) & ( ( 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 x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & b1 = x' + y' ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = x' & x = [0 ,y'] & b1 = x' - y' ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = y' & b1 = y' - x' ) ) & ( ( 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 x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & b1 = [0 ,(x' + y')] ) ) ) ;
func * x,y -> Element of REAL means :Def3: :: ARYTM_0:def 3
 ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' *' y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & it = [0 ,(x' *' y')] ) if ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & it = [0 ,(y' *' x')] ) if ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & it = y' *' x' ) if ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] )
otherwise it = 0 ;
existence
( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = y' *' x' ) ) & ( ( 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 b1 being Element of REAL st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b2 = x' *' y' ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b2 = [0 ,(x' *' y')] ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b2 = [0 ,(y' *' x')] ) implies b1 = b2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b2 = y' *' x' ) implies b1 = b2 ) & ( ( 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+ :] ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = y' *' x' ) ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = y' *' x' ) ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = y' *' x' ) ) ) ) by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 implies ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = [0 ,(x' *' y')] ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = [0 ,(y' *' x')] ) ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ex x', y' being Elemen