:: Introduction to Arithmetics
::  by Andrzej Trybulec
::
:: Received January 9, 2003
:: Copyright (c) 2003-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ARYTM_2, TARSKI, NUMBERS, ZFMISC_1, SUBSET_1, ARYTM_1,
      ARYTM_3, CARD_1, RELAT_1, FUNCOP_1, ORDINAL1, FUNCT_2, FUNCT_1, ARYTM_0,
      XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS;
 constructors FUNCT_4, ARYTM_1, NUMBERS, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, FUNCT_2, FUNCT_4, ARYTM_2, FUNCT_1, NUMBERS;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions ORDINAL1;
 equalities NUMBERS, TARSKI, ARYTM_3, ORDINAL1;
 expansions TARSKI, ORDINAL1;
 theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, XBOOLE_1, ORDINAL3,
      ARYTM_3, FUNCT_2, FUNCT_4, FUNCT_1, ENUMSET1, NUMBERS, XTUPLE_0;

begin :: Arithmetics

Lm1: for x being Element of REAL+ holds [0,x] in [:{0},REAL+:]
 proof 0 in {0} by TARSKI:def 1;
  hence thesis by ZFMISC_1:87;
 end;

theorem Th1:
  REAL+ c= REAL
proof
  REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7;
  hence thesis by ARYTM_2:3,ZFMISC_1:34;
end;

theorem Th2:
  for x being Element of REAL+ st x <> {} holds [{},x] in REAL
proof
  let x be Element of REAL+ such that
A1: x <> {};
A2: now
    assume [{},x] in {[{},{}]};
    then [{},x] = [{},{}] by TARSKI:def 1;
    hence contradiction by A1,XTUPLE_0:1;
  end;
  {} in {{}} by TARSKI:def 1;
  then [{},x] in [:{{}},REAL+:] by ZFMISC_1:87;
  then [{},x] in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 3;
  hence thesis by A2,XBOOLE_0:def 5;
end;

theorem Th3:
  for y being set st [{},y] in REAL holds y <> {}
proof
  let y be set such that
A1: [{},y] in REAL and
A2: y = {};
  [{},y] in {[{},{}]} by A2,TARSKI:def 1;
  hence contradiction by A1,XBOOLE_0:def 5;
end;

theorem Th4:
  for x,y being Element of REAL+ holds x - y in REAL
proof
  let x,y be Element of REAL+;
  per cases;
  suppose
    y <=' x;
    then x - y = x -' y by ARYTM_1:def 2;
    then x - y in REAL+;
    hence thesis by Th1;
  end;
  suppose
A1: not y <=' x;
    then x - y = [{},y -' x] by ARYTM_1:def 2;
    hence thesis by A1,Th2,ARYTM_1:9;
  end;
end;

theorem Th5:
  REAL+ misses [:{{}},REAL+:]
proof
  assume REAL+ meets [:{{}},REAL+:];
  then consider x being object such that
A1: x in REAL+ and
A2: x in [:{{}},REAL+:] by XBOOLE_0:3;
  consider x1,x2 being object such that
A3: x1 in {{}} and
  x2 in REAL+ and
A4: x = [x1,x2] by A2,ZFMISC_1:84;
  x1 = {} by A3,TARSKI:def 1;
  hence contradiction by A1,A4,ARYTM_2:3;
end;

begin  :: Real numbers

registration let x,y be object;
 cluster [x,y] -> non zero;
 coherence;
end;

theorem Th6:
  for x,y being Element of REAL+ st x - y = {} holds x = y
proof
  let x,y be Element of REAL+;
  assume
A1: x - y = {};
  0 <> [{},y -' x];
  then y <=' x & x -' y = {} by A1,ARYTM_1:def 2;
  hence thesis by ARYTM_1:10;
end;

Lm2:
  not ex a,b being set st 1 = [a,b]
proof
  let a,b be set;
  assume
A1: 1 = [a,b];
  {a} in {{a,b},{a}} by TARSKI:def 2;
  hence contradiction by A1,ORDINAL3:15,TARSKI:def 1;
end;

theorem Th7:
  for x,y,z being Element of REAL+ st x <> {} & x *' y = x *' z holds y = z
proof
  let x,y,z be Element of REAL+;
  assume that
A1: x <> {} and
A2: x *' y = x *' z;
  per cases;
  suppose
A3: z <=' y;
    then x *' (y -' z) = (x *' y) - (x *' z) by ARYTM_1:26
      .= {} by A2,ARYTM_1:18;
    then {} = y -' z by A1,ARYTM_1:2
      .= y - z by A3,ARYTM_1:def 2;
    hence thesis by Th6;
  end;
  suppose
A4: y <=' z;
    then x *' (z -' y) = x *' z - x *' y by ARYTM_1:26
      .= {} by A2,ARYTM_1:18;
    then {} = z -' y by A1,ARYTM_1:2
      .= z - y by A4,ARYTM_1:def 2;
    hence thesis by Th6;
  end;
end;

begin
Lm3: 0 in REAL by NUMBERS:19;

definition
  let x,y be Element of REAL;

  func +(x,y) -> Element of REAL means
  :Def1:
  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
  proof
    hereby
      assume x in REAL+ & y in REAL+;
      then reconsider x9=x, y9=y as Element of REAL+;
      reconsider IT = x9 + y9 as Element of REAL by Th1;
      take IT,x9,y9;
      thus x = x9 & y = y9 & IT = x9 + y9;
    end;
A1: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
    hereby
      assume x in REAL+;
      then reconsider x9=x as Element of REAL+;
      assume y in [:{0},REAL+:];
      then consider z,y9 being object such that
A2:   z in{0} and
A3:   y9 in REAL+ and
A4:   y = [z,y9] by ZFMISC_1:84;
      reconsider y9 as Element of REAL+ by A3;
      reconsider IT = x9 - y9 as Element of REAL by Th4;
      take IT,x9,y9;
      thus x = x9 & y = [0,y9] & IT = x9 - y9 by A2,A4,TARSKI:def 1;
    end;
    hereby
      assume y in REAL+;
      then reconsider y9=y as Element of REAL+;
      assume x in [:{0},REAL+:];
      then consider z,x9 being object such that
A5:   z in{0} and
A6:   x9 in REAL+ and
A7:   x = [z,x9] by ZFMISC_1:84;
      reconsider x9 as Element of REAL+ by A6;
      reconsider IT = y9 - x9 as Element of REAL by Th4;
      take IT,x9,y9;
      thus x = [0,x9] & y = y9 & IT = y9 - x9 by A5,A7,TARSKI:def 1;
    end;
    assume that
A8: not(x in REAL+ & y in REAL+) and
A9: not(x in REAL+ & y in [:{0},REAL+:]) and
A10: not(y in REAL+ & x in [:{0},REAL+:]);
A11: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
    then x in REAL+ or x in [:{0},REAL+:] by XBOOLE_0:def 3;
    then consider z1,x9 being object such that
A12: z1 in{0} and
A13: x9 in REAL+ and
A14: x = [z1,x9] by A1,A8,A9,XBOOLE_0:def 3,ZFMISC_1:84;
    y in REAL+ or y in [:{0},REAL+:] by A1,XBOOLE_0:def 3;
    then consider z2,y9 being object such that
A15: z2 in{0} and
A16: y9 in REAL+ and
A17: y = [z2,y9] by A11,A8,A10,XBOOLE_0:def 3,ZFMISC_1:84;
    reconsider x9 as Element of REAL+ by A13;
    reconsider y9 as Element of REAL+ by A16;
    x = [0,x9] by A12,A14,TARSKI:def 1;
    then x9 + y9 <> 0 by Th3,ARYTM_2:5;
    then reconsider IT = [0,y9 + x9] as Element of REAL by Th2;
    take IT,x9,y9;
    thus thesis by A12,A14,A15,A17,TARSKI:def 1;
  end;
  uniqueness
  proof
    let IT1,IT2 be Element of REAL;
    thus x in REAL+ & y in REAL+ & (ex x9,y9 being Element of REAL+ st x = x9
& y = y9 & IT1 = x9 + y9) & (ex x9,y9 being Element of REAL+ st x = x9 & y = y9
    & IT2 = x9 + y9) implies IT1 = IT2;
    thus x in REAL+ & y in [:{0},REAL+:] & (ex x9,y9 being Element of REAL+ st
x = x9 & y = [0,y9] &IT1 = x9 - y9) & (ex x99,y99 being Element of REAL+ st x =
    x99 & y = [0,y99] & IT2 = x99 - y99) implies IT1 = IT2 by XTUPLE_0:1;
    thus y in REAL+ & x in [:{0},REAL+:] & (ex x9,y9 being Element of REAL+ st
x = [0,x9] & y = y9 & IT1 = y9 - x9) & (ex x99,y99 being Element of REAL+ st x
    = [0,x99] & y = y99 & IT2 = y99 - x99) implies IT1 = IT2 by XTUPLE_0:1;
    assume that
    not(x in REAL+ & y in REAL+) and
    not(x in REAL+ & y in [:{0},REAL+:]) and
    not(y in REAL+ & x in [:{0},REAL+:]);
    given x9,y9 being Element of REAL+ such that
A18: x = [0,x9] and
A19: y = [0,y9] & IT1 = [0,x9+y9];
    given x99,y99 being Element of REAL+ such that
A20: x = [0,x99] and
A21: y = [0,y99] & IT2 = [0,x99+y99];
    x9 = x99 by A18,A20,XTUPLE_0:1;
    hence thesis by A19,A21,XTUPLE_0:1;
  end;
  consistency by Th5,XBOOLE_0:3;
  commutativity;
  func *(x,y) -> Element of REAL means
  :Def2:
  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
  proof
    hereby
      assume x in REAL+ & y in REAL+;
      then reconsider x9=x, y9=y as Element of REAL+;
      reconsider IT = x9 *' y9 as Element of REAL by Th1;
      take IT,x9,y9;
      thus x = x9 & y = y9 & IT = x9 *' y9;
    end;
    hereby
      assume x in REAL+;
      then reconsider x9=x as Element of REAL+;
      assume y in [:{0},REAL+:];
      then consider z,y9 being object such that
A22:  z in{0} and
A23:  y9 in REAL+ and
A24:  y = [z,y9] by ZFMISC_1:84;
      reconsider y9 as Element of REAL+ by A23;
      y = [0,y9] by A22,A24,TARSKI:def 1;
      then
A25:  y9 <> 0 by Th3;
      assume x <> 0;
      then reconsider IT = [0,x9 *' y9] as Element of REAL by A25,Th2,ARYTM_1:2
;
      take IT,x9,y9;
      thus x = x9 & y = [0,y9] & IT = [0,x9 *' y9] by A22,A24,TARSKI:def 1;
    end;
    hereby
      assume y in REAL+;
      then reconsider y9=y as Element of REAL+;
      assume x in [:{0},REAL+:];
      then consider z,x9 being object such that
A26:  z in{0} and
A27:  x9 in REAL+ and
A28:  x = [z,x9] by ZFMISC_1:84;
      reconsider x9 as Element of REAL+ by A27;
      x = [0,x9] by A26,A28,TARSKI:def 1;
      then
A29:  x9 <> 0 by Th3;
      assume y <> 0;
      then reconsider IT = [0,y9 *' x9] as Element of REAL by A29,Th2,ARYTM_1:2
;
      take IT,x9,y9;
      thus x = [0,x9] & y = y9 & IT = [0,y9 *' x9] by A26,A28,TARSKI:def 1;
    end;
    hereby
      assume x in [:{0},REAL+:];
      then consider z1,x9 being object such that
A30:  z1 in{0} and
A31:  x9 in REAL+ and
A32:  x = [z1,x9] by ZFMISC_1:84;
      reconsider x9 as Element of REAL+ by A31;
      assume y in [:{0},REAL+:];
      then consider z2,y9 being object such that
A33:  z2 in{0} and
A34:  y9 in REAL+ and
A35:  y = [z2,y9] by ZFMISC_1:84;
      reconsider y9 as Element of REAL+ by A34;
      reconsider IT = y9 *' x9 as Element of REAL by Th1;
      take IT,x9,y9;
      thus x = [0,x9] & y = [0,y9] & IT = y9 *' x9 by A30,A32,A33,A35,
TARSKI:def 1;
    end;
    thus thesis by Lm3;
  end;
  uniqueness
  proof
    let IT1,IT2 be Element of REAL;
    thus x in REAL+ & y in REAL+ & (ex x9,y9 being Element of REAL+ st x = x9
& y = y9 & IT1 = x9 *' y9) & (ex x9,y9 being Element of REAL+ st x = x9 & y =
    y9 & IT2 = x9 *' y9) implies IT1 = IT2;
    thus x in REAL+ & y in [:{0},REAL+:] & x <> 0 & (ex x9,y9 being Element of
REAL+ st x = x9 & y = [0,y9] & IT1 = [0,x9 *' y9]) & (ex x99,y99 being Element
of REAL+ st x = x99 & y = [0,y99] & IT2 = [0,x99 *' y99]) implies IT1 = IT2 by
XTUPLE_0:1;
    thus y in REAL+ & x in [:{0},REAL+:] & y <> 0 & (ex x9,y9 being Element of
REAL+ st x = [0,x9] & y = y9 & IT1 = [0,y9 *' x9]) & (ex x99,y99 being Element
of REAL+ st x = [0,x99] & y = y99 & IT2 = [0,y99 *' x99]) implies IT1 = IT2 by
XTUPLE_0:1;
    hereby
      assume that
      x in [:{0},REAL+:] and
      y in [:{0},REAL+:];
      given x9,y9 being Element of REAL+ such that
A36:  x = [0,x9] and
A37:  y = [0,y9] & IT1 = y9 *' x9;
      given x99,y99 being Element of REAL+ such that
A38:  x = [0,x99] and
A39:  y = [0,y99] & IT2 = y99 *' x99;
      x9 = x99 by A36,A38,XTUPLE_0:1;
      hence IT1 = IT2 by A37,A39,XTUPLE_0:1;
    end;
    thus thesis;
  end;
  consistency by Th5,XBOOLE_0:3;
  commutativity;
end;

reserve x,y for Element of REAL;

definition
  let x be Element of REAL;
  func opp x -> Element of REAL means
  :Def3:
  +(x,it) = 0;
  existence
  proof
    reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20;
A1: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
    per cases by A1,XBOOLE_0:def 3;
    suppose
A2:   x = 0;
      then reconsider x9 = x as Element of REAL+ by ARYTM_2:20;
      take x;
      x9 + x9 = 0 by A2,ARYTM_2:def 8;
      hence thesis by Def1,Lm3;
    end;
    suppose that
A3:   x in REAL+ and
A4:   x <> 0;
A5:   [0,x] <> [0,0] by A4,XTUPLE_0:1;
      0 in {0} by TARSKI:def 1;
      then
A6:   [0,x] in [:{0},REAL+:] by A3,ZFMISC_1:87;
      then [0,x] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
      then reconsider y = [0,x] as Element of REAL by A5
,ZFMISC_1:56;
      reconsider x9 = x as Element of REAL+ by A3;
A7:   x9 <=' x9;
      take y;
      z9 + x9 = x9 by ARYTM_2:def 8;
      then z9 = x9 -' x9 by A7,ARYTM_1:def 1;
      then 0 = x9 - x9 by A7,ARYTM_1:def 2;
      hence thesis by A6,Def1,Lm3;
    end;
    suppose
A8:   x in [:{0},REAL+:];
      then consider a,b being object such that
A9:   a in {0} and
A10:  b in REAL+ and
A11:  x = [a,b] by ZFMISC_1:84;
      reconsider y = b as Element of REAL by A10,Th1;
      take y;
      now
        per cases;
        case
          x in REAL+ & y in REAL+;
          hence ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 0 = x9 +
          y9 by A8,Th5,XBOOLE_0:3;
        end;
        case
          x in REAL+ & y in [:{0},REAL+:];
          hence
          ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & 0 = x9
          - y9 by A10,Th5,XBOOLE_0:3;
        end;
        case
          y in REAL+ & x in [:{0},REAL+:];
          reconsider x9 = b, y9 = y as Element of REAL+ by A10;
          take x9, y9;
          thus x = [0,x9] by A9,A11,TARSKI:def 1;
          thus y = y9;
          thus 0 = y9 - x9 by ARYTM_1:18;
        end;
        case
          not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},
          REAL+:]) & not (y in REAL+ & x in [:{0},REAL+:]);
          hence ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & 0
          = [0,y9+x9] by A8,A10;
        end;
      end;
      hence thesis by Def1,Lm3;
    end;
  end;
  uniqueness
  proof
    let y,z be Element of REAL such that
A12: +(x,y) = 0 and
A13: +(x,z) = 0;
    per cases;
    suppose
      x in REAL+ & y in REAL+ & z in REAL+;
      then
      ( ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 0 = x9 + y9)
& ex x9,y9 being Element of REAL+ st x = x9 & z = y9 & 0 = x9 + y9 by A12,A13
,Def1;
      hence thesis by ARYTM_2:11;
    end;
    suppose that
A14:  x in REAL+ and
A15:  y in REAL+ and
A16:  z in [:{0},REAL+:];
      consider x99,y99 being Element of REAL+ such that
A17:  x = x99 and
A18:  z = [0,y99] & 0 = x99 - y99 by A13,A14,A16,Def1;
      ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 0 = x9 + y9 by A12
,A14,A15,Def1;
      then
A19:  x99 = 0 by A17,ARYTM_2:5;
      [0,0] in {[0,0]} by TARSKI:def 1;
      then
A20:  not [0,0] in REAL by XBOOLE_0:def 5;
      z in REAL;
      hence thesis by A18,A19,A20,ARYTM_1:19;
    end;
    suppose that
A21:  x in REAL+ and
A22:  z in REAL+ and
A23:  y in [:{0},REAL+:];
      consider x99,y9 being Element of REAL+ such that
A24:  x = x99 and
A25:  y = [0,y9] & 0 = x99 - y9 by A12,A21,A23,Def1;
      ex x9,z9 being Element of REAL+ st x = x9 & z = z9 & 0 = x9 + z9 by A13
,A21,A22,Def1;
      then
A26:  x99 = 0 by A24,ARYTM_2:5;
      [0,0] in {[0,0]} by TARSKI:def 1;
      then
A27:  not [0,0] in REAL by XBOOLE_0:def 5;
      y in REAL;
      hence thesis by A25,A26,A27,ARYTM_1:19;
    end;
    suppose that
A28:  x in REAL+ and
A29:  y in [:{0},REAL+:] and
A30:  z in [:{0},REAL+:];
      consider x99,z9 being Element of REAL+ such that
A31:  x = x99 and
A32:  z = [0,z9] and
A33:  0 = x99 - z9 by A13,A28,A30,Def1;
      consider x9,y9 being Element of REAL+ such that
A34:  x = x9 and
A35:  y = [0,y9] and
A36:  0 = x9 - y9 by A12,A28,A29,Def1;
      y9 = x9 by A36,Th6
        .= z9 by A34,A31,A33,Th6;
      hence thesis by A35,A32;
    end;
    suppose that
A37:  z in REAL+ and
A38:  y in REAL+ and
A39:  x in [:{0},REAL+:];
      consider x99,z9 being Element of REAL+ such that
A40:  x = [0,x99] and
A41:  z = z9 and
A42:  0 = z9 - x99 by A13,A37,A39,Def1;
      consider x9,y9 being Element of REAL+ such that
A43:  x = [0,x9] and
A44:  y = y9 and
A45:  0 = y9 - x9 by A12,A38,A39,Def1;
      x9 = x99 by A43,A40,XTUPLE_0:1;
      then z9 = x9 by A42,Th6
        .= y9 by A45,Th6;
      hence thesis by A44,A41;
    end;
    suppose
      not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},
      REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]);
      then
      ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & 0 = [0
      ,x9+y9] by A12,Def1;
      hence thesis;
    end;
    suppose
      not(x in REAL+ & z in REAL+) & not(x in REAL+ & z in [:{0},
      REAL+:]) & not(z in REAL+ & x in [:{0},REAL+:]);
      then
      ex x9,z9 being Element of REAL+ st x = [0,x9] & z = [0,z9] & 0 = [0
      ,x9+z9] by A13,Def1;
      hence thesis;
    end;
  end;
  involutiveness;
  func inv x -> Element of REAL means
  :Def4:
  *(x,it) = 1 if x <> 0 otherwise it = 0;
  existence
  proof
    thus x <> 0 implies ex y st *(x,y) = 1
    proof
A46:  x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
      assume
A47:  x <> 0;
      per cases by A46,XBOOLE_0:def 3;
      suppose
        x in REAL+;
        then reconsider x9 = x as Element of REAL+;
        reconsider jj = 1 as Element of REAL by NUMBERS:19;

        consider y9 being Element of REAL+ such that
A48:    x9 *' y9 = jj by A47,ARYTM_2:14;
        reconsider y = y9 as Element of REAL by Th1;
        take y;
        thus thesis by A48,Def2;
      end;
      suppose
A49:    x in [:{0},REAL+:];
        not x in {[0,0]} by XBOOLE_0:def 5;
        then
A50:    x <> [0,0] by TARSKI:def 1;
        consider x1,x2 being object such that
        x1 in {0} and
A51:    x2 in REAL+ and
A52:    x = [x1,x2] by A49,ZFMISC_1:84;
        reconsider x2 as Element of REAL+ by A51;
        x1 in {0} by A49,A52,ZFMISC_1:87;
        then x2 <> 0 by A52,A50,TARSKI:def 1;
        then consider y2 being Element of REAL+ such that
A53:    x2 *' y2 = 1 by ARYTM_2:14;
A54:    now
          assume [0,y2] in {[0,0]};
          then [0,y2] = [0,0] by TARSKI:def 1;
          then y2 = 0 by XTUPLE_0:1;
          hence contradiction by A53,ARYTM_2:4;
        end;
A55:    [0,y2] in [:{0},REAL+:] by Lm1;
        then [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
        then reconsider y = [0,y2] as Element of REAL by A54
,XBOOLE_0:def 5;
        take y;
        consider x9,y9 being Element of REAL+ such that
A56:    x = [0,x9] and
A57:    y = [0,y9] and
A58:    *(x,y) = y9 *' x9 by A49,A55,Def2;
        y9 = y2 by A57,XTUPLE_0:1;
        hence thesis by A52,A53,A56,A58,XTUPLE_0:1;
      end;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let y,z be Element of REAL;
    thus x <> 0 & *(x,y) = 1 & *(x,z) = 1 implies y = z
    proof
      assume that
A59:  x <> 0 and
A60:  *(x,y) = 1 and
A61:  *(x,z) = 1;
A62:  for x,y being Element of REAL st *(x,y) =1 holds x <> 0
      proof
        let x,y be Element of REAL such that
A63:    *(x,y) =1 and
A64:    x = 0;
A65:    not x in [:{0},REAL+:] by A64,Th5,ARYTM_2:20,XBOOLE_0:3;
A66:    y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
        per cases by A66,XBOOLE_0:def 3;
        suppose
          y in REAL+;
          then ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 1 = x9 *'
          y9 by A63,A64,Def2,ARYTM_2:20;
          hence contradiction by A64,ARYTM_2:4;
        end;
        suppose
          y in [:{0},REAL+:];
          then not y in REAL+ by Th5,XBOOLE_0:3;
          hence contradiction by A63,A64,A65,Def2;
        end;
      end;
      then
A67:  y <> 0 by A60;
A68:  z <> 0 by A61,A62;
      per cases;
      suppose
        x in REAL+ & y in REAL+ & z in REAL+;
        then ( ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 1 = x9 *'
y9)& ex x9,y9 being Element of REAL+ st x = x9 & z = y9 & 1 = x9 *' y9 by A60
,A61,Def2;
        hence thesis by A59,Th7;
      end;
      suppose that
A69:    x in [:{0},REAL+:] and
A70:    y in [:{0},REAL+:] and
A71:    z in [:{0},REAL+:];
        consider x9,y9 being Element of REAL+ such that
A72:    x = [0,x9] and
A73:    y = [0,y9] & 1 = y9 *' x9 by A60,A69,A70,Def2;
        consider x99,z9 being Element of REAL+ such that
A74:    x = [0,x99] and
A75:    z = [0,z9] & 1 = z9 *' x99 by A61,A69,A71,Def2;
        x9 = x99 by A72,A74,XTUPLE_0:1;
        hence thesis by A72,A73,A75,Th3,Th7;
      end;
      suppose
        x in REAL+ & y in [:{0},REAL+:];
        then ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & 1 = [0,
        x9 *' y9] by A59,A60,Def2;
        hence thesis by Lm2;
      end;
      suppose
        x in [:{0},REAL+:] & y in REAL+;
        then ex x9,y9 being Element of REAL+ st x = [0,x9] & y = y9 & 1 = [0,
        y9 *' x9] by A60,A67,Def2;
        hence thesis by Lm2;
      end;
      suppose
        x in [:{0},REAL+:] & z in REAL+;
        then ex x9,z9 being Element of REAL+ st x = [0,x9] & z = z9 & 1 = [0,
        z9 *' x9] by A61,A68,Def2;
        hence thesis by Lm2;
      end;
      suppose
        x in REAL+ & z in [:{0},REAL+:];
        then ex x9,z9 being Element of REAL+ st x = x9 & z = [0,z9] & 1 = [0,
        x9 *' z9] by A59,A61,Def2;
        hence thesis by Lm2;
      end;
      suppose
        not (x in REAL+ & y in REAL+) & not (x in REAL+ & y in [:{0}
,REAL+:] & x <> 0) & not (y in REAL+ & x in [:{0},REAL+:] & y <> 0) & not (x in
        [:{0},REAL+:] & y in [:{0},REAL+:]);
        hence thesis by A60,Def2;
      end;
      suppose
        not (x in REAL+ & z in REAL+) & not (x in REAL+ & z in [:{0}
,REAL+:] & x <> 0) & not (z in REAL+ & x in [:{0},REAL+:] & z <> 0) & not (x in
        [:{0},REAL+:] & z in [:{0},REAL+:]);
        hence thesis by A61,Def2;
      end;
    end;
    thus thesis;
  end;
  consistency;
  involutiveness
  proof
    let x,y be Element of REAL;
    assume that
A76: y <> 0 implies *(y,x) = 1 and
A77: y = 0 implies x = 0;
    thus x <> 0 implies *(x,y) = 1 by A76,A77;
    assume
A78: x = 0;
A79: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
    assume
A80: y <> 0;
    per cases by A79,XBOOLE_0:def 3;
    suppose
      y in REAL+;
      then ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 1 = x9 *' y9
      by A76,A78,A80,Def2,ARYTM_2:20;
      hence contradiction by A78,ARYTM_2:4;
    end;
    suppose
A81:  y in [:{0},REAL+:];
A82:  not x in [:{0},REAL+:] by A78,Th5,ARYTM_2:20,XBOOLE_0:3;
      not y in REAL+ by A81,Th5,XBOOLE_0:3;
      hence contradiction by A76,A78,A80,A82,Def2;
    end;
  end;
end;

begin :: from COMPLEX1

Lm4: for x,y,z being set st [x,y] = {z} holds z = {x} & x = y
proof
  let x,y,z be set;
  assume
A1: [x,y] = {z};
  then {x} in {z} by TARSKI:def 2;
  hence
A2: z = {x} by TARSKI:def 1;
  {x,y} in {z} by A1,TARSKI:def 2;
  then {x,y} = z by TARSKI:def 1;
  hence thesis by A2,ZFMISC_1:5;
end;

reserve i,j,k for Element of NAT;
reserve a,b for Element of REAL;

theorem Th8:
  not (0,1)-->(a,b) in REAL
proof
  set IR = { A where A is Subset of RAT+: for r being Element of RAT+ st r in
  A holds (for s being Element of RAT+ st s <=' r holds s in A) & ex s being
  Element of RAT+ st s in A & r < s};
  set f = (0,1)-->(a,b);
A1: now
    f = {[0,a],[1,b]} by FUNCT_4:67;
    then
A2: [1,b] in f by TARSKI:def 2;
    assume f in [:{{}},REAL+:];
    then consider x,y being object such that
A3: x in {{}} and
    y in REAL+ and
A4: f = [x,y] by ZFMISC_1:84;
    x = 0 by A3,TARSKI:def 1;
    then per cases by A4,A2,TARSKI:def 2;
    suppose
      {{1,b},{1}} = {0};
      then 0 in {{1,b},{1}} by TARSKI:def 1;
      hence contradiction by TARSKI:def 2;
    end;
    suppose
      {{1,b},{1}} = {0,y};
      then 0 in {{1,b},{1}} by TARSKI:def 2;
      hence contradiction by TARSKI:def 2;
    end;
  end;
A5: f = {[0,a],[1,b]} by FUNCT_4:67;
  now
    assume f in {[i,j]: i,j are_coprime & j <> {}};
    then consider i,j such that
A6: f = [i,j] and
    i,j are_coprime and
    j <> {};
A7: {i} in f & {i,j} in f by A6,TARSKI:def 2;
A8: now
      assume i = j;
      then {i} = {i,j} by ENUMSET1:29;
      then
A9:  [i,j] = {{i}} by ENUMSET1:29;
      then [1,b] in {{i}} by A5,A6,TARSKI:def 2;
      then
A10:  [1,b] = {i} by TARSKI:def 1;
      [0,a] in {{i}} by A5,A6,A9,TARSKI:def 2;
      then [0,a] = {i} by TARSKI:def 1;
      hence contradiction by A10,XTUPLE_0:1;
    end;
    per cases by A5,A7,TARSKI:def 2;
    suppose
      {i,j} = [0,a] & {i} = [0,a];
      hence contradiction by A8,ZFMISC_1:5;
    end;
    suppose that
A11:  {i,j} = [0,a] and
A12:  {i} = [1,b];
      i in {i,j} by TARSKI:def 2;
      then i = {0,a} or i = {0} by A11,TARSKI:def 2;
      then
A13:  0 in i by TARSKI:def 1,def 2;
      i = {1} by A12,Lm4;
      hence contradiction by A13,TARSKI:def 1;
    end;
    suppose that
A14:  {i,j} = [1,b] and
A15:  {i} = [0,a];
      i in {i,j} by TARSKI:def 2;
      then i = {1,b} or i = {1} by A14,TARSKI:def 2;
      then
A16:  1 in i by TARSKI:def 1,def 2;
      i = {0} by A15,Lm4;
      hence contradiction by A16,TARSKI:def 1;
    end;
    suppose
      {i,j} = [1,b] & {i} = [1,b];
      hence contradiction by A8,ZFMISC_1:5;
    end;
  end;
  then
A17: not f in {[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1];
  not ex x,y being set st {[0,x],[1,y]} in IR
  proof
    given x,y being set such that
A18: {[0,x],[1,y]} in IR;
    consider A being Subset of RAT+ such that
A19: {[0,x],[1,y]} = A and
A20: for r being Element of RAT+ st r in A holds (for s being Element
of RAT+ st s <=' r holds s in A) & ex s being Element of RAT+ st s in A & r < s
    by A18;
    [0,x] in A & for r,s being Element of RAT+ st r in A & s <=' r holds
    s in A by A19,A20,TARSKI:def 2;
    then consider r1,r2,r3 being Element of RAT+ such that
A21: r1 in A and
A22: r2 in A and
A23: r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 by ARYTM_3:75;
A24: r2 = [0,x] or r2 = [1,y] by A19,A22,TARSKI:def 2;
    r1 = [0,x] or r1 = [1,y] by A19,A21,TARSKI:def 2;
    hence contradiction by A19,A23,A24,TARSKI:def 2;
  end;
  then
A25: not f in DEDEKIND_CUTS by A5,ARYTM_2:def 1;
  now
    assume f in omega;
    then {} in f by ORDINAL3:8;
    hence contradiction by A5,TARSKI:def 2;
  end;
  then not f in RAT+ by A17,XBOOLE_0:def 3;
  then not f in REAL+ by A25,ARYTM_2:def 2,XBOOLE_0:def 3;
  hence thesis by A1,XBOOLE_0:def 3;
end;

definition
  let x,y be Element of REAL;

  func [*x,y*] -> Element of COMPLEX equals
  :Def5:
  x if y = 0 otherwise (0,1)
  --> (x,y);
  consistency;
  coherence
  proof
    set z = (0,1)-->(x,y);
    thus y = 0 implies x is Element of COMPLEX by XBOOLE_0:def 3;
    assume
A1: y <> 0;
A2: now
      assume z in { r where r is Element of Funcs({0,1},REAL): r.1 = 0 };
      then ex r being Element of Funcs({0,1},REAL) st z = r & r.1 = 0;
      hence contradiction by A1,FUNCT_4:63;
    end;
    z in Funcs({0,1},REAL) by FUNCT_2:8;
    then
    z in Funcs({0,1},REAL) \ { r where r is Element of Funcs({0,1},REAL):
    r.1 = 0} by A2,XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

theorem
  for c being Element of COMPLEX ex r,s being Element of REAL st c = [*r ,s*]
proof
  let c be Element of COMPLEX;
  per cases;
  suppose
    c in REAL;
    then reconsider r=c, z=0 as Element of REAL by Lm3;
    take r,z;
    thus thesis by Def5;
  end;
  suppose
    not c in REAL;
    then
A1: c in Funcs({0,1},REAL) \ { x where x is Element of Funcs({0,1},REAL):
    x.1 = 0} by XBOOLE_0:def 3;
    then consider f being Function such that
A2: c = f and
A3: dom f = {0,1} and
A4: rng f c= REAL by FUNCT_2:def 2;
    1 in {0,1} by TARSKI:def 2;
    then
A5: f.1 in rng f by A3,FUNCT_1:3;
    0 in {0,1} by TARSKI:def 2;
    then f.0 in rng f by A3,FUNCT_1:3;
    then reconsider r = f.0, s = f.1 as Element of REAL by A4,A5;
    take r,s;
A6: c = (0,1)-->(r,s) by A2,A3,FUNCT_4:66;
    now
      assume s = 0;
      then (0,1)-->(r,s).1 = 0 by FUNCT_4:63;
      then c in { x where x is Element of Funcs({0,1},REAL): x.1 = 0} by A1,A6;
      hence contradiction by A1,XBOOLE_0:def 5;
    end;
    hence thesis by A6,Def5;
  end;
end;

theorem
  for x1,x2,y1,y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds
  x1 = y1 & x2 = y2
proof
  let x1,x2,y1,y2 be Element of REAL such that
A1: [*x1,x2*] = [*y1,y2*];
  per cases;
  suppose
A2: x2 = 0;
    then
A3: [*x1,x2*] = x1 by Def5;
A4: now
      assume y2 <> 0;
      then x1 = (0,1) --> (y1,y2) by A1,A3,Def5;
      hence contradiction by Th8;
    end;
    hence x1 = y1 by A1,A3,Def5;
    thus thesis by A2,A4;
  end;
  suppose
    x2 <> 0;
    then
A5: [*y1,y2*] = (0,1) --> (x1,x2) by A1,Def5;
    now
      assume y2 = 0;
      then [*y1,y2*] = y1 by Def5;
      hence contradiction by A5,Th8;
    end;
    then [*y1,y2*] = (0,1) --> (y1,y2) by Def5;
    hence thesis by A5,FUNCT_4:68;
  end;
end;

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

theorem Th11:
  for x,o being Element of REAL st o = 0 holds +(x,o) = x
proof
  reconsider y9 = 0 as Element of REAL+ by ARYTM_2:20;
  let x,o being Element of REAL such that
A1: o = 0;
  per cases;
  suppose
    x in REAL+;
    then reconsider x9 = x as Element of REAL+;
    x9 = x9 + y9 by ARYTM_2:def 8;
    hence thesis by A1,Def1;
  end;
  suppose
A2: not x in REAL+;
    x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5;
    then
A3: x in [:{{}},REAL+:] by A2,XBOOLE_0:def 3;
    then consider x1,x2 being object such that
A4: x1 in {{}} and
A5: x2 in REAL+ and
A6: x = [x1,x2] by ZFMISC_1:84;
    reconsider x9 = x2 as Element of REAL+ by A5;
A7: x1 = 0 by A4,TARSKI:def 1;
    then x = y9 - x9 by A6,Th3,ARYTM_1:19;
    hence thesis by A1,A3,A6,A7,Def1;
  end;
end;

theorem Th12:
  for x,o being Element of REAL st o = 0 holds *(x,o) = 0
proof
  let x,o being Element of REAL such that
A1: o = 0;
  per cases;
  suppose
    x in REAL+;
    then reconsider x9 = x, y9 = 0 as Element of REAL+ by ARYTM_2:20;
    0 = x9 *' y9 by ARYTM_2:4;
    hence thesis by A1,Def2;
  end;
  suppose
A2: not x in REAL+;
    not o in [:{{}},REAL+:] by A1,Th5,ARYTM_2:20,XBOOLE_0:3;
    hence thesis by A1,A2,Def2;
  end;
end;

theorem Th13:
  for x,y,z being Element of REAL holds *(x,*(y,z)) = *(*(x,y),z)
proof
  let x,y,z be Element of REAL;
  reconsider o = 0 as Element of REAL by Lm3;

  per cases;
  suppose that
A1: x in REAL+ and
A2: y in REAL+ and
A3: z in REAL+;
A4: ex x99,y99 being Element of REAL+ st x = x99 & y = y99 & *(x,y) = x99
    *' y99 by A1,A2,Def2;
    then
A5: ex xy99,z99 being Element of REAL+ st *(x,y) = xy99 & z = z99 & *(*(x,y
    ),z) = xy99 *' z99 by A3,Def2;
A6: ex y9,z9 being Element of REAL+ st y = y9 & z = z9 & *( y,z) = y9 *' z9
    by A2,A3,Def2;
    then
    ex x9,yz9 being Element of REAL+ st x = x9 & *(y,z) = yz9 & *(x,*(y,z))
    = x9 *' yz9 by A1,Def2;
    hence thesis by A6,A4,A5,ARYTM_2:12;
  end;
  suppose that
A7: x in REAL+ & x <> 0 and
A8: y in RR and
A9: z in REAL+ & z <> 0;
    consider y9,z9 being Element of REAL+ such that
A10: y = [0,y9] and
A11: z = z9 and
A12: *(y,z) = [0,z9 *' y9] by A8,A9,Def2;
    *(y,z) in [:{0},REAL+:] by A12,Lm1;
    then consider x9,yz9 being Element of REAL+ such that
A13: x = x9 and
A14: *(y,z) = [0,yz9] & *(x,*(y,z) ) = [0,x9 *' yz9] by A7,Def2;
    consider x99,y99 being Element of REAL+ such that
A15: x = x99 and
A16: y = [0,y99] and
A17: *(x,y) = [0,x99 *' y99] by A7,A8,Def2;
A18: y9 = y99 by A10,A16,XTUPLE_0:1;
    *(x,y) in [:{0},REAL+:] by A17,Lm1;
    then consider xy99,z99 being Element of REAL+ such that
A19: *(x,y) = [0,xy99] and
A20: z = z99 and
A21: *(*(x,y),z) = [0,z99 *' xy99] by A9,Def2;
    thus *(x,*(y,z)) = [0,x9 *' (y9 *' z9)] by A12,A14,XTUPLE_0:1
      .= [0,(x99 *' y99) *' z99] by A11,A13,A15,A20,A18,ARYTM_2:12
      .= *(*(x,y),z) by A17,A19,A21,XTUPLE_0:1;
  end;
  suppose that
A22: x in RR and
A23: y in REAL+ & y <> 0 and
A24: z in REAL+ & z <> 0;
    consider y9,z9 being Element of REAL+ such that
A25: y = y9 & z = z9 and
A26: *(y,z) = y9 *' z9 by A23,A24,Def2;
    y9 *' z9 <> 0 by A23,A24,A25,ARYTM_1:2;
    then consider x9,yz9 being Element of REAL+ such that
A27: x = [0,x9] and
A28: *(y,z) = yz9 & *(x,*(y,z)) = [0,yz9 *' x9] by A22,A26,Def2;
    consider x99,y99 being Element of REAL+ such that
A29: x = [0,x99] and
A30: y = y99 and
A31: *(x,y) = [0,y99 *' x99] by A22,A23,Def2;
    *(x,y) in [:{0},REAL+:] by A31,Lm1;
    then consider xy99,z99 being Element of REAL+ such that
A32: *(x,y) = [0,xy99] and
A33: z = z99 and
A34: *(*(x,y),z) = [0,z99 *' xy99] by A24,Def2;
    x9 = x99 by A27,A29,XTUPLE_0:1;
    hence *(x,*(y,z)) = [0,(x99 *' y99) *' z99] by A25,A26,A28,A30,A33,
ARYTM_2:12
      .= *(*(x,y),z) by A31,A32,A34,XTUPLE_0:1;
  end;
  suppose that
A35: x in RR and
A36: y in RR and
A37: z in REAL+ & z <> 0;
    consider x99,y99 being Element of REAL+ such that
A38: x = [0,x99] and
A39: y = [0,y99] and
A40: *(x,y) = y99 *' x99 by A35,A36,Def2;
    consider y9,z9 being Element of REAL+ such that
A41: y = [0,y9] and
A42: z = z9 and
A43: *(y,z) = [0,z9 *' y9] by A36,A37,Def2;
A44: y9 = y99 by A41,A39,XTUPLE_0:1;
    *(y,z) in [:{0},REAL+:] by A43,Lm1;
    then consider x9,yz9 being Element of REAL+ such that
A45: x = [0,x9] and
A46: *(y,z) = [0,yz9] & *(x,*(y,z)) = yz9 *' x9 by A35,Def2;
A47: x9 = x99 by A45,A38,XTUPLE_0:1;
A48: ex xy99,z99 being Element of REAL+ st *(x,y) = xy99 & z = z99 & *(*(x,
    y),z) = xy99 *' z99 by A37,A40,Def2;
    thus *(x,*(y,z)) = x9 *' (y9 *' z9) by A43,A46,XTUPLE_0:1
      .= *(*(x,y),z) by A42,A40,A48,A47,A44,ARYTM_2:12;
  end;
  suppose that
A49: x in REAL+ & x <> 0 and
A50: y in REAL+ & y <> 0 and
A51: z in RR;
A52: ex x99,y99 being Element of REAL+ st x = x99 & y = y99 & *(x,y) = x99
    *' y99 by A49,A50,Def2;
    then *(x,y) <> 0 by A49,A50,ARYTM_1:2;
    then consider xy99,z99 being Element of REAL+ such that
A53: *(x,y) = xy99 and
A54: z = [0,z99] and
A55: *(*(x,y),z) = [0,xy99 *' z99] by A51,A52,Def2;
    consider y9,z9 being Element of REAL+ such that
A56: y = y9 and
A57: z = [0,z9] and
A58: *(y,z) = [0,y9 *' z9] by A50,A51,Def2;
A59: z9 = z99 by A57,A54,XTUPLE_0:1;
    *(y,z) in [:{0},REAL+:] by A58,Lm1;
    then consider x9,yz9 being Element of REAL+ such that
A60: x = x9 and
A61: *(y,z) = [0,yz9] & *(x,*(y,z)) = [0,x9 *' yz9] by A49,Def2;
    thus *(x,*(y,z)) = [0,x9 *' (y9 *' z9)] by A58,A61,XTUPLE_0:1
      .= *(*(x,y),z) by A56,A60,A52,A53,A55,A59,ARYTM_2:12;
  end;
  suppose that
A62: x in REAL+ & x <> 0 and
A63: y in RR and
A64: z in RR;
    consider y9,z9 being Element of REAL+ such that
A65: y = [0,y9] and
A66: z = [0,z9] and
A67: *(y,z) = z9 *' y9 by A63,A64,Def2;
A68: ex x9,yz9 being Element of REAL+ st x = x9 & *(y,z) = yz9 & *(x,*(y,z)
    ) = x9 *' yz9 by A62,A67,Def2;
    consider x99,y99 being Element of REAL+ such that
A69: x = x99 and
A70: y = [0,y99] and
A71: *(x,y) = [0,x99 *' y99] by A62,A63,Def2;
A72: y9 = y99 by A65,A70,XTUPLE_0:1;
    *(x,y) in [:{0},REAL+:] by A71,Lm1;
    then consider xy99,z99 being Element of REAL+ such that
A73: *(x,y) = [0,xy99] and
A74: z = [0,z99] and
A75: *(*(x,y),z) = z99 *' xy99 by A64,Def2;
    z9 = z99 by A66,A74,XTUPLE_0:1;
    hence *(x,*(y,z)) = (x99 *' y99) *' z99 by A67,A68,A69,A72,ARYTM_2:12
      .= *(*(x,y),z) by A71,A73,A75,XTUPLE_0:1;
  end;
  suppose that
A76: y in REAL+ & y <> 0 and
A77: x in RR and
A78: z in RR;
    consider x99,y99 being Element of REAL+ such that
A79: x = [0,x99] and
A80: y = y99 and
A81: *(x,y) = [0,y99 *' x99] by A76,A77,Def2;
    consider y9,z9 being Element of REAL+ such that
A82: y = y9 and
A83: z = [0,z9] and
A84: *(y,z) = [0,y9 *' z9] by A76,A78,Def2;
    [0,y9 *' z9] in [:{0},REAL+:] by Lm1;
    then consider x9,yz9 being Element of REAL+ such that
A85: x = [0,x9] and
A86: *(y,z) = [0,yz9] & *(x,*(y,z)) = yz9 *' x9 by A77,A84,Def2;
A87: x9 = x99 by A85,A79,XTUPLE_0:1;
    *(x,y) in [:{0},REAL+:] by A81,Lm1;
    then consider xy99,z99 being Element of REAL+ such that
A88: *(x,y) = [0,xy99] and
A89: z = [0,z99] and
A90: *(*(x,y),z) = z99 *' xy99 by A78,Def2;
A91: z9 = z99 by A83,A89,XTUPLE_0:1;
    thus *(x,*(y,z)) = x9 *' (y9 *' z9) by A84,A86,XTUPLE_0:1
      .= (x99 *' y99) *' z99 by A82,A80,A87,A91,ARYTM_2:12
      .= *(*(x,y),z) by A81,A88,A90,XTUPLE_0:1;
  end;
  suppose that
A92: x in RR and
A93: y in RR and
A94: z in RR;
    consider y9,z9 being Element of REAL+ such that
A95: y = [0,y9] and
A96: z = [0,z9] and
A97: *(y,z) = z9 *' y9 by A93,A94,Def2;
    not y in {[0,0]} by XBOOLE_0:def 5;
    then
A98: y9 <> 0 by A95,TARSKI:def 1;
    not z in {[0,0]} by XBOOLE_0:def 5;
    then z9 <> 0 by A96,TARSKI:def 1;
    then *(z,y) <> 0 by A97,A98,ARYTM_1:2;
    then consider x9,yz9 being Element of REAL+ such that
A99: x = [0,x9] and
A100: *(y,z) = yz9 & *(x,*(y,z)) = [0,yz9 *' x9] by A92,A97,Def2;
    consider x99,y99 being Element of REAL+ such that
A101: x = [0,x99] and
A102: y = [0,y99] and
A103: *(x,y) = y99 *' x99 by A92,A93,Def2;
A104: x9 = x99 by A99,A101,XTUPLE_0:1;
A105: y9 = y99 by A95,A102,XTUPLE_0:1;
    not y in {[0,0]} by XBOOLE_0:def 5;
    then
A106: y9 <> 0 by A95,TARSKI:def 1;
    not x in {[0,0]} by XBOOLE_0:def 5;
    then x9 <> 0 by A99,TARSKI:def 1;
    then *(x,y) <> 0 by A103,A104,A105,A106,ARYTM_1:2;
    then consider xy99,z99 being Element of REAL+ such that
A107: *(x,y) = xy99 and
A108: z = [0,z99] and
A109: *(*(x,y),z) = [0,xy99 *' z99] by A94,A103,Def2;
    z9 = z99 by A96,A108,XTUPLE_0:1;
    hence thesis by A97,A100,A103,A104,A105,A107,A109,ARYTM_2:12;
  end;
  suppose
A110: x = 0;
    hence *(x,*(y,z)) = 0 by Th12
      .= *(o,z) by Th12
      .= *(*(x,y),z) by A110,Th12;
  end;
  suppose
A111: y = 0;
    hence *(x,*(y,z)) = *(x,o) by Th12
      .= 0 by Th12
      .= *(o,z) by Th12
      .= *(*(x,y),z) by A111,Th12;
  end;
  suppose
A112: z = 0;
    hence *(x,*(y,z)) = *(x,o) by Th12
      .= 0 by Th12
      .= *(*(x,y),z) by A112,Th12;
  end;
  suppose
A113: not( x in REAL+ & y in REAL+ & z in REAL+) & not(x in REAL+ & y
in RR & z in REAL+) & not(y in REAL+ & x in RR & z in REAL+) & not(x in RR & y
in RR & z in REAL+) & not( x in REAL+ & y in REAL+ & z in RR) & not(x in REAL+
& y in RR & z in RR) & not(y in REAL+ & x in RR & z in RR) & not(x in RR & y in
    RR & z in RR);
    REAL = (REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) by XBOOLE_1:42
      .= REAL+ \/ RR by ARYTM_2:3,ZFMISC_1:57;
    hence thesis by A113,XBOOLE_0:def 3;
  end;
end;

theorem Th14:
  for x,y,z being Element of REAL holds *(x,+(y,z)) = +(*(x,y),*(x ,z))
proof
  let x,y,z be Element of REAL;
  reconsider o = 0 as Element of REAL by Lm3;

  per cases;
  suppose
A1: x = 0;
    hence *(x,+(y,z)) = 0 by Th12
      .= +(o,o) by Th11
      .= +(*(x,y),o) by A1,Th12
      .= +(*(x,y),*(x,z)) by A1,Th12;
  end;
  suppose that
A2: x in REAL+ and
A3: y in REAL+ & z in REAL+;
A4: (ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & *( x,y) = x9 *'
y9 )& ex x99,z9 being Element of REAL+ st x = x99 & z = z9 & *(x,z) = x99 *' z9
    by A2,A3,Def2;
    then
A5: ex xy9,xz9 being Element of REAL+ st *(x,y) = xy9 & *(x, z) = xz9 & +(*
    (x,y),*(x,z)) = xy9 + xz9 by Def1;
A6: ex y99,z99 being Element of REAL+ st y = y99 & z = z99 & +(y,z) = y99 +
    z99 by A3,Def1;
    then
    ex x999,yz9 being Element of REAL+ st x = x999 & +(y,z) = yz9 & *(x,+(y
    ,z)) = x999 *' yz9 by A2,Def2;
    hence thesis by A4,A5,A6,ARYTM_2:13;
  end;
  suppose that
A7: x in REAL+ & x <> 0 and
A8: y in REAL+ and
A9: z in RR;
    consider y99,z99 being Element of REAL+ such that
A10: y = y99 and
A11: z = [0,z99] and
A12: +(y,z) = y99 - z99 by A8,A9,Def1;
    consider x9,y9 being Element of REAL+ such that
A13: x = x9 & y = y9 and
A14: *(x,y) = x9 *' y9 by A7,A8,Def2;
    consider x99,z9 being Element of REAL+ such that
A15: x = x99 and
A16: z = [0,z9] and
A17: *(x,z) = [0,x99 *' z9] by A7,A9,Def2;
    *(x,z) in [:{0},REAL+:] by A17,Lm1;
    then
A18: ex xy9,xz9 being Element of REAL+ st *(x,y) = xy9 & *(x, z) = [0,xz9]
    & +(*(x,y),*(x,z)) = xy9 - xz9 by A14,Def1;
A19: z9 = z99 by A16,A11,XTUPLE_0:1;
    now
      per cases;
      suppose
A20:    z99 <=' y99;
        then
A21:    +(y,z) = y99 -' z99 by A12,ARYTM_1:def 2;
        then
        ex x999,yz9 being Element of REAL+ st x = x999 & +(y,z) = yz9 & *(
        x,+(y,z)) = x999 *' yz9 by A7,Def2;
        hence
        *(x,+(y,z)) = (x9 *' y9) - (x99 *' z9) by A13,A15,A10,A19,A20,A21,
ARYTM_1:26
          .= +(*(x,y),*(x,z)) by A14,A17,A18,XTUPLE_0:1;
      end;
      suppose
A22:    not z99 <=' y99;
        then
A23:    +(y,z) = [0,z99 -' y99] by A12,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then consider x999,yz9 being Element of REAL+ such that
A24:    x = x999 and
A25:    +(y,z) = [0,yz9] & *(x,+(y,z)) = [0,x999 *' yz9] by A7,Def2;
        thus *(x,+(y,z)) = [0,x999 *' (z99 -' y99)] by A23,A25,XTUPLE_0:1
          .= (x9 *' y9) - (x99 *' z9) by A7,A13,A15,A10,A19,A22,A24,ARYTM_1:27
          .= +(*(x,y),*(x,z)) by A14,A17,A18,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A26: x in REAL+ & x <> 0 and
A27: z in REAL+ and
A28: y in RR;
    consider z99,y99 being Element of REAL+ such that
A29: z = z99 and
A30: y = [0,y99] and
A31: +(z,y) = z99 - y99 by A27,A28,Def1;
    consider x9,z9 being Element of REAL+ such that
A32: x = x9 & z = z9 and
A33: *(x,z) = x9 *' z9 by A26,A27,Def2;
    consider x99,y9 being Element of REAL+ such that
A34: x = x99 and
A35: y = [0,y9] and
A36: *(x,y) = [0,x99 *' y9] by A26,A28,Def2;
    *(x,y) in [:{0},REAL+:] by A36,Lm1;
    then
A37: ex xz9,xy9 being Element of REAL+ st *(x,z) = xz9 & *(x, y) = [0,xy9]
    & +(*(x,z),*(x,y)) = xz9 - xy9 by A33,Def1;
A38: y9 = y99 by A35,A30,XTUPLE_0:1;
    now
      per cases;
      suppose
A39:    y99 <=' z99;
        then
A40:    +(z,y) = z99 -' y99 by A31,ARYTM_1:def 2;
        then
        ex x999,zy9 being Element of REAL+ st x = x999 & +(z,y) = zy9 & *(
        x,+(z,y)) = x999 *' zy9 by A26,Def2;
        hence
        *(x,+(z,y)) = (x9 *' z9) - (x99 *' y9) by A32,A34,A29,A38,A39,A40,
ARYTM_1:26
          .= +(*(x,z),*(x,y)) by A33,A36,A37,XTUPLE_0:1;
      end;
      suppose
A41:    not y99 <=' z99;
        then
A42:    +(z,y) = [0,y99 -' z99] by A31,ARYTM_1:def 2;
        then +(z,y) in [:{0},REAL+:] by Lm1;
        then consider x999,zy9 being Element of REAL+ such that
A43:    x = x999 and
A44:    +(z,y) = [0,zy9] & *(x,+(z,y)) = [0,x999 *' zy9] by A26,Def2;
        thus *(x,+(z,y)) = [0,x999 *' (y99 -' z99)] by A42,A44,XTUPLE_0:1
          .= (x9 *' z9) - (x99 *' y9) by A26,A32,A34,A29,A38,A41,A43,ARYTM_1:27
          .= +(*(x,z),*(x,y)) by A33,A36,A37,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A45: x in REAL+ & x <> 0 and
A46: y in RR and
A47: z in RR;
    ( not(y in REAL+ & z in [:{0},REAL+:]))& not(y in [:{0},REAL+:] & z
    in REAL+) by A46,A47,Th5,XBOOLE_0:3;
    then consider y99,z99 being Element of REAL+ such that
A48: y = [0,y99] and
A49: z = [0,z99] and
A50: +(y,z) = [0,y99 + z99] by A46,Def1;
    +(y,z) in [:{0},REAL+:] by A50,Lm1;
    then consider x999,yz9 being Element of REAL+ such that
A51: x = x999 and
A52: +(y,z) = [0,yz9] & *(x,+(y,z)) = [0,x999 *' yz9] by A45,Def2;
    consider x9,y9 being Element of REAL+ such that
A53: x = x9 and
A54: y = [0,y9] and
A55: *(x,y) = [0,x9 *' y9] by A45,A46,Def2;
A56: y9 = y99 by A54,A48,XTUPLE_0:1;
    consider x99,z9 being Element of REAL+ such that
A57: x = x99 and
A58: z = [0,z9] and
A59: *(x,z) = [0,x99 *' z9] by A45,A47,Def2;
    *(x,z) in [:{0},REAL+:] by A59,Lm1;
    then
A60: not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3;
    *(x,y) in [:{0},REAL+:] by A55,Lm1;
    then not(*(x,y) in REAL+ & *(x,z) in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
    then consider xy9,xz9 being Element of REAL+ such that
A61: *(x,y) = [0,xy9] and
A62: *(x,z) = [0,xz9] & +(*(x,y),*(x,z)) = [0,xy9 + xz9] by A55,A60,Def1,Lm1;
A63: xy9 = x9 *' y9 by A55,A61,XTUPLE_0:1;
A64: z9 = z99 by A58,A49,XTUPLE_0:1;
    thus *(x,+(y,z)) = [0,x999 *' (y99 + z99)] by A50,A52,XTUPLE_0:1
      .= [0,(x9 *' y9) + (x9 *' z9)] by A53,A51,A56,A64,ARYTM_2:13
      .= +(*(x,y),*(x,z)) by A53,A57,A59,A62,A63,XTUPLE_0:1;
  end;
  suppose that
A65: x in RR and
A66: y in REAL+ and
A67: z in REAL+;
    consider y99,z99 being Element of REAL+ such that
A68: y = y99 and
A69: z = z99 and
A70: +(y,z) = y99 + z99 by A66,A67,Def1;
    now
      per cases;
      suppose that
A71:    y <> 0 and
A72:    z <> 0;
        consider x99,z9 being Element of REAL+ such that
A73:    x = [0,x99] and
A74:    z = z9 and
A75:    *(x,z) = [0,z9 *' x99] by A65,A67,A72,Def2;
        y99 + z99 <> 0 by A69,A72,ARYTM_2:5;
        then consider x999,yz9 being Element of REAL+ such that
A76:    x = [0,x999] and
A77:    +(y,z) = yz9 & *(x,+(y,z)) = [0,yz9 *' x999] by A65,A70,Def2;
        consider x9,y9 being Element of REAL+ such that
A78:    x = [0,x9] and
A79:    y = y9 and
A80:    *(x,y) = [0,y9 *' x9] by A65,A66,A71,Def2;
A81:    x99 = x999 by A73,A76,XTUPLE_0:1;
        *(x,z) in [:{0},REAL+:] by A75,Lm1;
        then
A82:    not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3;
        *(x,y) in [:{0},REAL+:] by A80,Lm1;
        then not(*(x,y) in REAL+ & *(x,z) in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider xy9,xz9 being Element of REAL+ such that
A83:    *(x,y) = [0,xy9] and
A84:    *(x,z) = [0,xz9] & +(*(x,y),*(x,z)) = [0,xy9 + xz9]
              by A80,A82,Def1,Lm1;
A85:    xy9 = x9 *' y9 by A80,A83,XTUPLE_0:1;
        x9 = x99 by A78,A73,XTUPLE_0:1;
        hence *(x,+(y,z)) = [0,(x9 *' y9) + (x99 *' z9)] by A68,A69,A70,A79,A74
,A77,A81,ARYTM_2:13
          .= +(*(x,y),*(x,z)) by A75,A84,A85,XTUPLE_0:1;
      end;
      suppose
A86:    x = 0;
        hence *(x,+(y,z)) = 0 by Th12
          .= +(o,o) by Th11
          .= +(*(x,y),o) by A86,Th12
          .= +(*(x,y),*(x,z)) by A86,Th12;
      end;
      suppose
A87:    z = 0;
        hence *(x,+(y,z)) = *(x,y) by Th11
          .= +(*(x,y),*(x,z)) by A87,Th11,Th12;
      end;
      suppose
A88:    y = 0;
        hence *(x,+(y,z)) = *(x,z) by Th11
          .= +(*(x,y),*(x,z)) by A88,Th11,Th12;
      end;
    end;
    hence thesis;
  end;
  suppose that
A89: x in RR and
A90: y in REAL+ and
A91: z in RR;
    consider x99,z9 being Element of REAL+ such that
A92: x = [0,x99] and
A93: z = [0,z9] and
A94: *(x,z) = z9 *' x99 by A89,A91,Def2;
    now
      per cases;
      suppose
        y <> 0;
        then consider x9,y9 being Element of REAL+ such that
A95:    x = [0,x9] and
A96:    y = y9 and
A97:    *(x,y) = [0,y9 *' x9] by A89,A90,Def2;
        *(x,y) in [:{0},REAL+:] by A97,Lm1;
        then consider xy9,xz9 being Element of REAL+ such that
A98:    *(x,y) = [0,xy9] and
A99:    *(x,z) = xz9 & +(*(x,y),*(x,z)) = xz9 - xy9 by A94,Def1;
        consider y99,z99 being Element of REAL+ such that
A100:   y = y99 and
A101:   z = [0,z99] and
A102:   +(y,z) = y99 - z99 by A91,A96,Def1;
A103:   z9 = z99 by A93,A101,XTUPLE_0:1;
        now
          per cases;
          suppose
A104:       z99 <=' y99;
            then
A105:       +(y,z) = y99 -' z99 by A102,ARYTM_1:def 2;
            now
              per cases;
              suppose
A106:           +(y,z) <> 0;
                then consider x999,yz9 being Element of REAL+ such that
A107:           x = [0,x999] and
A108:           +(y,z) = yz9 & *(x,+(y,z)) = [0,yz9 *' x999] by A89,A105,Def2;
                not x in {[0,0]} by XBOOLE_0:def 5;
                then
A109:           x999 <> 0 by A107,TARSKI:def 1;
A110:           z9 = z99 by A93,A101,XTUPLE_0:1;
A111:           x9 = x99 by A92,A95,XTUPLE_0:1;
                x99 = x999 by A92,A107,XTUPLE_0:1;
                hence *(x,+(y,z)) = (x9 *' z9) - (x9 *' y9) by A96,A100,A104
,A105,A106,A108,A111,A110,A109,ARYTM_1:28
                  .= +(*(x,y),*(x,z)) by A94,A97,A98,A99,A111,XTUPLE_0:1;
              end;
              suppose
A112:           +(y,z) = 0;
                then
A113:           y99 = z99 by A104,A105,ARYTM_1:10;
A114:           xy9 = x9 *' y9 & x9 = x99 by A92,A95,A97,A98,XTUPLE_0:1;
                thus *(x,+(y,z)) = 0 by A112,Th12
                  .= +(*(x,y),*(x,z)) by A94,A96,A100,A99,A103,A113,A114,
ARYTM_1:18;
              end;
            end;
            hence thesis;
          end;
          suppose
A115:       not z99 <=' y99;
            then
A116:       +(y,z) = [0,z99 -' y99] by A102,ARYTM_1:def 2;
            then +(y,z) in [:{0},REAL+:] by Lm1;
            then consider x999,yz9 being Element of REAL+ such that
A117:       x = [0,x999] and
A118:       +(y,z) = [0,yz9] & *(x,+(y,z)) = yz9 *' x999 by A89,Def2;
A119:       x99 = x999 by A92,A117,XTUPLE_0:1;
A120:       x9 = x99 by A92,A95,XTUPLE_0:1;
            thus *(x,+(y,z)) = x999 *' (z99 -' y99) by A116,A118,XTUPLE_0:1
              .= (x99 *' z9) - (x9 *' y9) by A96,A100,A103,A115,A120,A119,
ARYTM_1:26
              .= +(*(x,y),*(x,z)) by A94,A97,A98,A99,XTUPLE_0:1;
          end;
        end;
        hence thesis;
      end;
      suppose
A121:   y = 0;
        hence *(x,+(y,z)) = *(x,z) by Th11
          .= +(*(x,y),*(x,z)) by A121,Th11,Th12;
      end;
    end;
    hence thesis;
  end;
  suppose that
A122: x in RR and
A123: z in REAL+ and
A124: y in RR;
    consider x99,y9 being Element of REAL+ such that
A125: x = [0,x99] and
A126: y = [0,y9] and
A127: *(x,y) = y9 *' x99 by A122,A124,Def2;
    now
      per cases;
      suppose
        z <> 0;
        then consider x9,z9 being Element of REAL+ such that
A128:   x = [0,x9] and
A129:   z = z9 and
A130:   *(x,z) = [0,z9 *' x9] by A122,A123,Def2;
        *(x,z) in [:{0},REAL+:] by A130,Lm1;
        then consider xz9,xy9 being Element of REAL+ such that
A131:   *(x,z) = [0,xz9] and
A132:   *(x,y) = xy9 & +(*(x,z),*(x,y)) = xy9 - xz9 by A127,Def1;
        consider z99,y99 being Element of REAL+ such that
A133:   z = z99 and
A134:   y = [0,y99] and
A135:   +(z,y) = z99 - y99 by A124,A129,Def1;
A136:   y9 = y99 by A126,A134,XTUPLE_0:1;
        now
          per cases;
          suppose
A137:       y99 <=' z99;
            then
A138:       +(z,y) = z99 -' y99 by A135,ARYTM_1:def 2;
            now
              per cases;
              suppose
A139:           +(z,y) <> 0;
                then consider x999,zy9 being Element of REAL+ such that
A140:           x = [0,x999] and
A141:           +(z,y) = zy9 & *(x,+(z,y)) = [0,zy9 *' x999] by A122,A138,Def2;
                not x in {[0,0]} by XBOOLE_0:def 5;
                then
A142:           x999 <> 0 by A140,TARSKI:def 1;
A143:           y9 = y99 by A126,A134,XTUPLE_0:1;
A144:           x9 = x99 by A125,A128,XTUPLE_0:1;
                x99 = x999 by A125,A140,XTUPLE_0:1;
                hence *(x,+(z,y)) = (x9 *' y9) - (x9 *' z9) by A129,A133,A137
,A138,A139,A141,A144,A143,A142,ARYTM_1:28
                  .= +(*(x,z),*(x,y)) by A127,A130,A131,A132,A144,XTUPLE_0:1;
              end;
              suppose
A145:           +(z,y) = 0;
                then
A146:           z99 = y99 by A137,A138,ARYTM_1:10;
A147:           xz9 = x9 *' z9 & x9 = x99 by A125,A128,A130,A131,XTUPLE_0:1;
                thus *(x,+(z,y)) = 0 by A145,Th12
                  .= +(*(x,z),*(x,y)) by A127,A129,A133,A132,A136,A146,A147,
ARYTM_1:18;
              end;
            end;
            hence thesis;
          end;
          suppose
A148:       not y99 <=' z99;
            then
A149:       +(z,y) = [0,y99 -' z99] by A135,ARYTM_1:def 2;
            then +(z,y) in [:{0},REAL+:] by Lm1;
            then consider x999,zy9 being Element of REAL+ such that
A150:       x = [0,x999] and
A151:       +(z,y) = [0,zy9] & *(x,+(z,y)) = zy9 *' x999 by A122,Def2;
A152:       x99 = x999 by A125,A150,XTUPLE_0:1;
A153:       x9 = x99 by A125,A128,XTUPLE_0:1;
            thus *(x,+(y,z)) = x999 *' (y99 -' z99) by A149,A151,XTUPLE_0:1
              .= (x99 *' y9) - (x9 *' z9) by A129,A133,A136,A148,A153,A152,
ARYTM_1:26
              .= +(*(x,y),*(x,z)) by A127,A130,A131,A132,XTUPLE_0:1;
          end;
        end;
        hence thesis;
      end;
      suppose
A154:   z = 0;
        hence *(x,+(y,z)) = *(x,y) by Th11
          .= +(*(x,y),*(x,z)) by A154,Th11,Th12;
      end;
    end;
    hence thesis;
  end;
  suppose that
A155: x in RR and
A156: y in RR and
A157: z in RR;
    ( not(y in REAL+ & z in [:{0},REAL+:]))& not(y in [:{0},REAL+:] & z
    in REAL+) by A156,A157,Th5,XBOOLE_0:3;
    then consider y99,z99 being Element of REAL+ such that
A158: y = [0,y99] and
A159: z = [0,z99] and
A160: +(y,z) = [0,y99 + z99] by A156,Def1;
    consider x99,z9 being Element of REAL+ such that
A161: x = [0,x99] and
A162: z = [0,z9] and
A163: *(x,z) = z9 *' x99 by A155,A157,Def2;
A164: z9 = z99 by A162,A159,XTUPLE_0:1;
    consider x9,y9 being Element of REAL+ such that
A165: x = [0,x9] and
A166: y = [0,y9] and
A167: *(x,y) = y9 *' x9 by A155,A156,Def2;
A168: y9 = y99 by A166,A158,XTUPLE_0:1;
    +(y,z) in [:{0},REAL+:] by A160,Lm1;
    then consider x999,yz9 being Element of REAL+ such that
A169: x = [0,x999] and
A170: +(y,z) = [0,yz9] & *(x,+(y,z)) = yz9 *' x999 by A155,Def2;
A171: x9 = x999 by A165,A169,XTUPLE_0:1;
A172: (ex xy9,xz9 being Element of REAL+ st *(x,y) = xy9 & *(x, z) = xz9 &
+(*(x, y),*(x,z)) = xy9 + xz9 )& x9 = x99 by A165,A167,A161,A163,Def1,
XTUPLE_0:1;
    thus *(x,+(y,z)) = x999 *' (y99 + z99) by A160,A170,XTUPLE_0:1
      .= +(*(x,y),*(x,z)) by A167,A163,A172,A171,A168,A164,ARYTM_2:13;
  end;
  suppose
A173: not(x in REAL+ & y in REAL+ & z in REAL+) & not(x in REAL+ & y
in REAL+ & z in RR) & not(x in REAL+ & y in RR & z in REAL+) & not(x in REAL+ &
y in RR & z in RR) & not(x in RR & y in REAL+ & z in REAL+) & not(x in RR & y
in REAL+ & z in RR) & not(x in RR & y in RR & z in REAL+) & not(x in RR & y in
    RR & z in RR);
    REAL = (REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) by XBOOLE_1:42
      .= REAL+ \/ RR by ARYTM_2:3,ZFMISC_1:57;
    hence thesis by A173,XBOOLE_0:def 3;
  end;
end;

theorem
  for x,y being Element of REAL holds *(opp x,y) = opp *(x,y)
proof
  let x,y be Element of REAL;
  +(*(opp x,y),*(x,y)) = *(+(opp x,x), y) by Th14
    .= 0 by Th12,Def3;
  hence thesis by Def3;
end;

theorem Th16:
  for x being Element of REAL holds *(x,x) in REAL+
proof
  let x be Element of REAL;
A1: x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5;
  per cases by A1,XBOOLE_0:def 3;
  suppose
    x in REAL+;
    then
    ex x9,y9 being Element of REAL+ st x = x9 & x = y9 & *(x,x) = x9 *' y9
    by Def2;
    hence thesis;
  end;
  suppose
    x in [:{0},REAL+:];
    then
    ex x9,y9 being Element of REAL+ st x = [0,x9] & x = [0,y9] & *(x,x) =
    y9 *' x9 by Def2;
    hence thesis;
  end;
end;

theorem
  for x,y st +(*(x,x),*(y,y)) = 0 holds x = 0
proof
  let x,y such that
A1: +(*(x,x),*(y,y)) = 0;
  *(x,x) in REAL+ & *(y,y) in REAL+ by Th16;
  then consider x9,y9 being Element of REAL+ such that
A2: *(x,x) = x9 and
  *(y,y) = y9 and
A3: 0 = x9 + y9 by A1,Def1;
A4: x9 = 0 by A3,ARYTM_2:5;
A5: x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5;
  per cases by A5,XBOOLE_0:def 3;
  suppose
    x in REAL+;
    then ex x9,y9 being Element of REAL+ st x = x9 & x = y9 & 0 = x9 *' y9 by
A2,A4,Def2;
    hence thesis by ARYTM_1:2;
  end;
  suppose
    x in [:{0},REAL+:];
    then consider x9,y9 being Element of REAL+ such that
A6: x = [0,x9] and
A7: x = [0,y9] and
A8: 0 = y9 *' x9 by A2,A4,Def2;
    x9 = y9 by A6,A7,XTUPLE_0:1;
    then x9 = 0 by A8,ARYTM_1:2;
    then x in {[0,0]} by A6,TARSKI:def 1;
    hence thesis by XBOOLE_0:def 5;
  end;
end;

theorem Th18:
  for x,y,z being Element of REAL st x <> 0 & *(x,y) = 1 & *(x,z)
  = 1 holds y = z
proof
  let x,y,z be Element of REAL;
  assume that
A1: x <> 0 and
A2: *(x,y) = 1 and
A3: *(x,z) = 1;
  thus y = inv x by A1,A2,Def4
    .= z by A1,A3,Def4;
end;

theorem Th19:
  for x,y st y = 1 holds *(x,y) = x
proof
  let x,y such that
A1: y = 1;
  per cases;
  suppose
    x = 0;
    hence thesis by Th12;
  end;
  suppose
A2: x <> 0;
A3: now
      assume
A4:   inv x = 0;
      thus 1 = *(x, inv x) by A2,Def4
        .= 0 by A4,Th12;
    end;
A5: ex x9,y9 being Element of REAL+ st y = x9 & y = y9 & *(y,y) = x9 *' y9
    by A1,Def2,ARYTM_2:20;
A6: *(x,inv x) = 1 by A2,Def4;
    *(*(x,y), inv x) = *(*(x,inv x), y) by Th13
      .= *(y,y) by A1,A2,Def4
      .= 1 by A1,A5,ARYTM_2:15;
    hence thesis by A3,A6,Th18;
  end;
end;

theorem
  for x,y st y <> 0 holds *(*(x,y),inv y) = x
proof
  reconsider jj = 1 as Element of REAL by NUMBERS:19;

  let x,y such that
A1: y <> 0;
  thus *(*(x,y),inv y) = *(x,*(y,inv y)) by Th13
    .= *(x,jj) by A1,Def4
    .= x by Th19;
end;

theorem Th21:
  for x,y st *(x,y) = 0 holds x = 0 or y = 0
proof
  reconsider jj = 1 as Element of REAL by NUMBERS:19;
  let x,y such that
A1: *(x,y) = 0 and
A2: x <> 0;
A3: *(x, inv x) = 1 by A2,Def4;
  thus y = *(jj,y) by Th19
    .= *(*(x,y),inv x) by A3,Th13
    .= 0 by A1,Th12;
end;

theorem
  for x,y holds inv *(x,y) = *(inv x, inv y)
proof
  reconsider jj = 1 as Element of REAL by NUMBERS:19;
  let x,y;
  per cases;
  suppose
A1: x = 0 or y = 0;
    then
A2: inv x = 0 or inv y = 0 by Def4;
    *(x,y) = 0 by A1,Th12;
    hence inv *(x,y) = 0 by Def4
      .= *(inv x, inv y) by A2,Th12;
  end;
  suppose that
A3: x <> 0 and
A4: y <> 0;
A5: *(x,y) <> 0 by A3,A4,Th21;
A6: *(x,inv x) = 1 by A3,Def4;
A7: *(y,inv y) = 1 by A4,Def4;
    *(*(x,y),*(inv x, inv y)) = *(*(*(x,y),inv x), inv y) by Th13
      .= *(*(jj,y), inv y) by A6,Th13
      .= 1 by A7,Th19;
    hence thesis by A5,Def4;
  end;
end;

theorem Th23:
  for x,y,z being Element of REAL holds +(x,+(y,z)) = +(+(x,y),z)
proof
  let x,y,z be Element of REAL;
A1: x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:]
     by XBOOLE_0:def 5;
A2: z in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
  per cases by A1,A2,XBOOLE_0:def 3;
  suppose that
A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+;
A6: ex x99,y99 being Element of REAL+ st x = x99 & y = y99 & +(x,y) = x99 +
    y99 by A3,A4,Def1;
    then
A7: ex xy99,z99 being Element of REAL+ st +(x,y) = xy99 & z = z99 & +(+(x,
    y),z) = xy99 + z99 by A5,Def1;
A8: ex y9,z9 being Element of REAL+ st y = y9 & z = z9 & +( y,z) = y9 + z9
    by A4,A5,Def1;
    then
    ex x9,yz9 being Element of REAL+ st x = x9 & +(y,z) = yz9 & +(x,+(y,z))
    = x9 + yz9 by A3,Def1;
    hence thesis by A8,A6,A7,ARYTM_2:6;
  end;
  suppose that
A9: x in REAL+ and
A10: y in REAL+ and
A11: z in [:{0},REAL+:];
A12: ex x99,y99 being Element of REAL+ st x = x99 & y = y99 & +(x,y) = x99
    + y99 by A9,A10,Def1;
    then consider xy99,z99 being Element of REAL+ such that
A13: +(x,y) = xy99 and
A14: z = [0,z99] and
A15: +(+(x,y),z) = xy99 - z99 by A11,Def1;
    consider y9,z9 being Element of REAL+ such that
A16: y = y9 and
A17: z = [0,z9] and
A18: +(y,z) = y9 - z9 by A10,A11,Def1;
A19: z9 = z99 by A17,A14,XTUPLE_0:1;
    now
      per cases;
      suppose
A20:    z9 <=' y9;
        then
A21:    +(y,z) = y9 -' z9 by A18,ARYTM_1:def 2;
        then
        ex x9,yz9 being Element of REAL+ st x = x9 & +(y,z) = yz9 & +(x,+(
        y,z)) = x9 + yz9 by A9,Def1;
        hence thesis by A16,A12,A13,A15,A19,A20,A21,ARYTM_1:20;
      end;
      suppose
A22:    not z9 <=' y9;
        then
A23:    +(y,z) = [0,z9 -' y9] by A18,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then consider x9,yz9 being Element of REAL+ such that
A24:    x = x9 and
A25:    +(y,z) = [0,yz9] & +(x,+(y,z)) = x9 - yz9 by A9,Def1;
        thus +(x,+(y,z)) = x9 - (z9 -' y9) by A23,A25,XTUPLE_0:1
          .= +(+(x,y),z) by A16,A12,A13,A15,A19,A22,A24,ARYTM_1:21;
      end;
    end;
    hence thesis;
  end;
  suppose that
A26: x in REAL+ and
A27: y in [:{0},REAL+:] and
A28: z in REAL+;
    consider x99,y99 being Element of REAL+ such that
A29: x = x99 and
A30: y = [0,y99] and
A31: +(x,y) = x99 - y99 by A26,A27,Def1;
    consider z9,y9 being Element of REAL+ such that
A32: z = z9 and
A33: y = [0,y9] and
A34: +(y,z) = z9 - y9 by A27,A28,Def1;
A35: y9 = y99 by A33,A30,XTUPLE_0:1;
    now
      per cases;
      suppose that
A36:    y9 <=' x99 and
A37:    y9 <=' z9;
A38:    +(y,z) = z9 -' y9 by A34,A37,ARYTM_1:def 2;
        then consider x9,yz9 being Element of REAL+ such that
A39:    x = x9 and
A40:    +(y,z) = yz9 & +(x,+(y,z)) = x9 + yz9 by A26,Def1;
A41:    +(x,y) = x9 -' y9 by A29,A31,A35,A36,A39,ARYTM_1:def 2;
        then
        ex z99,xy99 being Element of REAL+ st z = z99 & +(x,y) = xy99 & +(
        z,+(x,y)) = z99 + xy99 by A28,Def1;
        hence thesis by A32,A29,A36,A37,A38,A39,A40,A41,ARYTM_1:12;
      end;
      suppose that
A42:    y9 <=' x99 and
A43:    not y9 <=' z9;
A44:    +(x,y) = x99 -' y9 by A31,A35,A42,ARYTM_1:def 2;
        then
A45:    ex z99,xy99 being Element of REAL+ st z = z99 & +(x,y) = xy99 & +(
        z,+(x,y)) = z99 + xy99 by A28,Def1;
A46:    +(y,z) = [0,y9 -' z9] by A34,A43,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then consider x9,yz9 being Element of REAL+ such that
A47:    x = x9 and
A48:    +(y,z) = [0,yz9] & +(x,+(y,z)) = x9 - yz9 by A26,Def1;
        thus +(x,+(y,z)) = x9 - (y9 -' z9) by A46,A48,XTUPLE_0:1
          .= +(+(x,y),z) by A32,A29,A42,A43,A47,A44,A45,ARYTM_1:22;
      end;
      suppose that
A49:    not y9 <=' x99 and
A50:    y9 <=' z9;
A51:    +(y,x) = [0,y9 -' x99] by A31,A35,A49,ARYTM_1:def 2;
        then +(y,x) in [:{0},REAL+:] by Lm1;
        then consider z99,yx99 being Element of REAL+ such that
A52:    z = z99 and
A53:    +(y,x) = [0,yx99] & +(z,+(y,x)) = z99 - yx99 by A28,Def1;
A54:    +(z,y) = z9 -' y9 by A34,A50,ARYTM_1:def 2;
        then
        ex x9,zy99 being Element of REAL+ st x = x9 & +(z,y) = zy99 & +(x,
        +(z,y)) = x9 + zy99 by A26,Def1;
        hence +(x,+(y,z)) = z99 - (y9 -' x99) by A32,A29,A49,A50,A52,A54,
ARYTM_1:22
          .= +(+(x,y),z) by A51,A53,XTUPLE_0:1;
      end;
      suppose that
A55:    not y9 <=' x99 and
A56:    not y9 <=' z9;
A57:    +(y,z) = [0,y9 -' z9] by A34,A56,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then consider x9,yz9 being Element of REAL+ such that
A58:    x = x9 and
A59:    +(y,z) = [0,yz9] & +(x,+(y,z)) = x9 - yz9 by A26,Def1;
A60:    +(y,x) = [0,y9 -' x99] by A31,A35,A55,ARYTM_1:def 2;
        then +(y,x) in [:{0},REAL+:] by Lm1;
        then consider z99,yx99 being Element of REAL+ such that
A61:    z = z99 and
A62:    +(y,x) = [0,yx99] & +(z,+(y,x)) = z99 - yx99 by A28,Def1;
        thus +(x,+(y,z)) = x9 - (y9 -' z9) by A57,A59,XTUPLE_0:1
          .= z99 - (y9 -' x99) by A32,A29,A55,A56,A61,A58,ARYTM_1:23
          .= +(+(x,y),z) by A60,A62,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A63: x in REAL+ and
A64: y in [:{0},REAL+:] and
A65: z in [:{0},REAL+:];
    ( not(z in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & z in [:{0},
    REAL+:]) by A64,A65,Th5,XBOOLE_0:3;
    then consider y9,z9 being Element of REAL+ such that
A66: y = [0,y9] and
A67: z = [0,z9] and
A68: +(y,z) = [0,y9 + z9] by A64,Def1;
    +(y,z) in [:{0},REAL+:] by A68,Lm1;
    then consider x9,yz9 being Element of REAL+ such that
A69: x = x9 and
A70: +(y,z) = [0,yz9] and
A71: +(x,+(y,z)) = x9 - yz9 by A63,Def1;
    consider x99,y99 being Element of REAL+ such that
A72: x = x99 and
A73: y = [0,y99] and
A74: +(x,y) = x99 - y99 by A63,A64,Def1;
A75: y9 = y99 by A66,A73,XTUPLE_0:1;
    now
      per cases;
      suppose
A76:    y99 <=' x99;
        then
A77:    +(x,y) = x99 -' y99 by A74,ARYTM_1:def 2;
        then consider xy99,z99 being Element of REAL+ such that
A78:    +(x,y) = xy99 and
A79:    z = [0,z99] and
A80:    +(+(x,y),z) = xy99 - z99 by A65,Def1;
A81:    z9 = z99 by A67,A79,XTUPLE_0:1;
        thus +(x,+(y,z)) = x9 - (y9 + z9) by A68,A70,A71,XTUPLE_0:1
          .= +(+(x,y),z) by A72,A69,A75,A76,A77,A78,A80,A81,ARYTM_1:24;
      end;
      suppose
A82:    not y99 <=' x99;
A83:    not(z in REAL+ & +(x,y) in [:{0},REAL+:]) by A65,Th5,XBOOLE_0:3;
A84:    +(x,y) = [0,y99 -' x99] by A74,A82,ARYTM_1:def 2;
        then +(x,y) in [:{0},REAL+:] by Lm1;
        then not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider xy99,z99 being Element of REAL+ such that
A85:    +(x,y) = [0,xy99] and
A86:    z = [0,z99] and
A87:    +(+(x,y),z) = [0,xy99 + z99] by A84,A83,Def1,Lm1;
A88:    z9 = z99 by A67,A86,XTUPLE_0:1;
A89:    yz9 = z9 + y9 by A68,A70,XTUPLE_0:1;
        then y99 <=' yz9 by A75,ARYTM_2:19;
        then not yz9 <=' x9 by A72,A69,A82,ARYTM_1:3;
        hence +(x,+(y,z)) = [0,z9 + y9 -' x9] by A71,A89,ARYTM_1:def 2
          .= [0,z99 + (y99 -' x99)] by A72,A69,A75,A82,A88,ARYTM_1:13
          .= +(+(x,y),z) by A84,A85,A87,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A90: z in REAL+ and
A91: y in REAL+ and
A92: x in [:{0},REAL+:];
A93: ex z99,y99 being Element of REAL+ st z = z99 & y = y99 & +(z,y) = z99
    + y99 by A90,A91,Def1;
    then consider zy99,x99 being Element of REAL+ such that
A94: +(z,y) = zy99 and
A95: x = [0,x99] and
A96: +(+(z,y),x) = zy99 - x99 by A92,Def1;
    consider y9,x9 being Element of REAL+ such that
A97: y = y9 and
A98: x = [0,x9] and
A99: +(y,x) = y9 - x9 by A91,A92,Def1;
A100: x9 = x99 by A98,A95,XTUPLE_0:1;
    now
      per cases;
      suppose
A101:   x9 <=' y9;
        then
A102:   +(y,x) = y9 -' x9 by A99,ARYTM_1:def 2;
        then ex z9,yx9 being Element of REAL+ st z = z9 & +(y,x) = yx9 & +(z,+
        (y,x)) = z9 + yx9 by A90,Def1;
        hence +(z,+(y,x)) = +(+(z,y),x) by A97,A93,A94,A96,A100,A101,A102,
ARYTM_1:20;
      end;
      suppose
A103:   not x9 <=' y9;
        then
A104:   +(y,x) = [0,x9 -' y9] by A99,ARYTM_1:def 2;
        then +(y,x) in [:{0},REAL+:] by Lm1;
        then consider z9,yx9 being Element of REAL+ such that
A105:   z = z9 and
A106:   +(y,x) = [0,yx9] & +(z,+(y,x)) = z9 - yx9 by A90,Def1;
        thus +(z,+(y,x)) = z9 - (x9 -' y9) by A104,A106,XTUPLE_0:1
          .= +(+(z,y),x) by A97,A93,A94,A96,A100,A103,A105,ARYTM_1:21;
      end;
    end;
    hence thesis;
  end;
  suppose that
A107: x in [:{0},REAL+:] and
A108: y in REAL+ and
A109: z in [:{0},REAL+:];
    consider y9,z9 being Element of REAL+ such that
A110: y = y9 and
A111: z = [0,z9] and
A112: +(y,z) = y9 - z9 by A108,A109,Def1;
    consider x99,y99 being Element of REAL+ such that
A113: x = [0,x99] and
A114: y = y99 and
A115: +(x,y) = y99 - x99 by A107,A108,Def1;
    now
      per cases;
      suppose that
A116:   x99 <=' y99 and
A117:   z9 <=' y9;
A118:   +(y,z) = y9 -' z9 by A112,A117,ARYTM_1:def 2;
        then consider x9,yz9 being Element of REAL+ such that
A119:   x = [0,x9] and
A120:   +(y,z) = yz9 & +(x,+(y,z)) = yz9 - x9 by A107,Def1;
A121:   x9 = x99 by A113,A119,XTUPLE_0:1;
        then
A122:   +(x,y) = y9 -' x9 by A110,A114,A115,A116,ARYTM_1:def 2;
        then consider z99,xy99 being Element of REAL+ such that
A123:   z = [0,z99] and
A124:   +(x,y) = xy99 & +(z,+(x,y)) = xy99 - z99 by A109,Def1;
        z9 = z99 by A111,A123,XTUPLE_0:1;
        hence thesis by A110,A114,A116,A117,A118,A120,A121,A122,A124,ARYTM_1:25
;
      end;
      suppose that
A125:   not x99 <=' y99 and
A126:   z9 <=' y9;
A127:   not(z in REAL+ & +(x,y) in [:{0},REAL+:]) by A109,Th5,XBOOLE_0:3;
A128:   +(y,x) = [0,x99 -' y99] by A115,A125,ARYTM_1:def 2;
        then +(y,x) in [:{0},REAL+:] by Lm1;
        then not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider z99,yx9 being Element of REAL+ such that
A129:   z = [0,z99] and
A130:   +(y,x) = [0,yx9] & +(z,+(y,x)) = [0,z99 + yx9] by A128,A127,Def1,Lm1;
A131:   z9 = z99 by A111,A129,XTUPLE_0:1;
A132:   +(y,z) = y9 -' z9 by A112,A126,ARYTM_1:def 2;
        then consider x9,yz9 being Element of REAL+ such that
A133:   x = [0,x9] and
A134:   +(y,z) = yz9 and
A135:   +(x,+(y,z)) = yz9 - x9 by A107,Def1;
A136:   x9 = x99 by A113,A133,XTUPLE_0:1;
        yz9 <=' y9 by A132,A134,ARYTM_1:11;
        then not x9 <=' yz9 by A110,A114,A125,A136,ARYTM_1:3;
        hence +(x,+(y,z)) = [0,x9 -' (y9 -' z9)] by A132,A134,A135,
ARYTM_1:def 2
          .= [0,x99 -' y99 + z99] by A110,A114,A125,A126,A136,A131,ARYTM_1:14
          .= +(+(x,y),z) by A128,A130,XTUPLE_0:1;
      end;
      suppose that
A137:   not z9 <=' y9 and
A138:   x99 <=' y99;
A139:   not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A107,Th5,XBOOLE_0:3;
A140:   +(y,z) = [0,z9 -' y9] by A112,A137,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider x9,yz99 being Element of REAL+ such that
A141:   x = [0,x9] and
A142:   +(y,z) = [0,yz99] & +(x,+(y,z)) = [0,x9 + yz99] by A140,A139,Def1,Lm1;
A143:   x99 = x9 by A113,A141,XTUPLE_0:1;
A144:   +(y,x) = y99 -' x99 by A115,A138,ARYTM_1:def 2;
        then consider z99,yx99 being Element of REAL+ such that
A145:   z = [0,z99] and
A146:   +(y,x) = yx99 and
A147:   +(z,+(y,x)) = yx99 - z99 by A109,Def1;
A148:   z99 = z9 by A111,A145,XTUPLE_0:1;
        yx99 <=' y99 by A144,A146,ARYTM_1:11;
        then
A149:   not z99 <=' yx99 by A110,A114,A137,A148,ARYTM_1:3;
        thus +(x,+(y,z)) = [0,z9 -' y9 + x9] by A140,A142,XTUPLE_0:1
          .= [0,z99 -' (y99 -' x99)] by A110,A114,A137,A138,A148,A143,
ARYTM_1:14
          .= +(+(x,y),z) by A144,A146,A147,A149,ARYTM_1:def 2;
      end;
      suppose that
A150:   not x99 <=' y99 and
A151:   not z9 <=' y9;
A152:   not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A107,Th5,XBOOLE_0:3;
A153:   not(z in REAL+ & +(x,y) in [:{0},REAL+:]) by A109,Th5,XBOOLE_0:3;
A154:   +(y,x) = [0,x99 -' y99] by A115,A150,ARYTM_1:def 2;
        then +(y,x) in [:{0},REAL+:] by Lm1;
        then not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider z99,yx9 being Element of REAL+ such that
A155:   z = [0,z99] and
A156:   +(y,x) = [0,yx9] & +(z,+(y,x)) = [0,z99 + yx9] by A154,A153,Def1,Lm1;
A157:   z9 = z99 by A111,A155,XTUPLE_0:1;
A158:   +(y,z) = [0,z9 -' y9] by A112,A151,ARYTM_1:def 2;
        then +(y,z) in [:{0},REAL+:] by Lm1;
        then not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider x9,yz99 being Element of REAL+ such that
A159:   x = [0,x9] and
A160:   +(y,z) = [0,yz99] & +(x,+(y,z)) = [0,x9 + yz99] by A158,A152,Def1,Lm1;
A161:   x9 = x99 by A113,A159,XTUPLE_0:1;
        thus +(x,+(y,z)) = [0,z9 -' y9 + x9] by A158,A160,XTUPLE_0:1
          .= [0,x99 -' y99 + z99] by A110,A114,A150,A151,A157,A161,ARYTM_1:15
          .= +(+(x,y),z) by A154,A156,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A162: z in REAL+ and
A163: y in [:{0},REAL+:] and
A164: x in [:{0},REAL+:];
    ( not(x in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & x in [:{0}
    ,REAL+:]) by A163,A164,Th5,XBOOLE_0:3;
    then consider y9,x9 being Element of REAL+ such that
A165: y = [0,y9] and
A166: x = [0,x9] and
A167: +(y,x) = [0,y9 + x9] by A163,Def1;
    +(y,x) in [:{0},REAL+:] by A167,Lm1;
    then consider z9,yx9 being Element of REAL+ such that
A168: z = z9 and
A169: +(y,x) = [0,yx9] and
A170: +(z,+(y,x)) = z9 - yx9 by A162,Def1;
    consider z99,y99 being Element of REAL+ such that
A171: z = z99 and
A172: y = [0,y99] and
A173: +(z,y) = z99 - y99 by A162,A163,Def1;
A174: y9 = y99 by A165,A172,XTUPLE_0:1;
    now
      per cases;
      suppose
A175:   y99 <=' z99;
        then
A176:   +(z,y) = z99 -' y99 by A173,ARYTM_1:def 2;
        then consider zy99,x99 being Element of REAL+ such that
A177:   +(z,y) = zy99 and
A178:   x = [0,x99] and
A179:   +(+(z,y),x) = zy99 - x99 by A164,Def1;
A180:   x9 = x99 by A166,A178,XTUPLE_0:1;
        thus +(z,+(y,x)) = z9 - (y9 + x9) by A167,A169,A170,XTUPLE_0:1
          .= +(+(z,y),x) by A171,A168,A174,A175,A176,A177,A179,A180,ARYTM_1:24;
      end;
      suppose
A181:   not y99 <=' z99;
A182:   not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A164,Th5,XBOOLE_0:3;
A183:   +(z,y) = [0,y99 -' z99] by A173,A181,ARYTM_1:def 2;
        then +(z,y) in [:{0},REAL+:] by Lm1;
        then not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
        then consider zy99,x99 being Element of REAL+ such that
A184:   +(z,y) = [0,zy99] and
A185:   x = [0,x99] and
A186:   +(+(z,y),x) = [0,zy99 + x99] by A183,A182,Def1,Lm1;
A187:   x9 = x99 by A166,A185,XTUPLE_0:1;
A188:   yx9 = x9 + y9 by A167,A169,XTUPLE_0:1;
        then y99 <=' yx9 by A174,ARYTM_2:19;
        then not yx9 <=' z9 by A171,A168,A181,ARYTM_1:3;
        hence +(z,+(y,x)) = [0,x9 + y9 -' z9] by A170,A188,ARYTM_1:def 2
          .= [0,x99 + (y99 -' z99)] by A171,A168,A174,A181,A187,ARYTM_1:13
          .= +(+(z,y),x) by A183,A184,A186,XTUPLE_0:1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A189: x in [:{0},REAL+:] and
A190: y in [:{0},REAL+:] and
A191: z in [:{0},REAL+:];
A192: not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A189,Th5,XBOOLE_0:3;
    ( not(z in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & z in [:{0}
    ,REAL+:]) by A190,A191,Th5,XBOOLE_0:3;
    then consider y9,z9 being Element of REAL+ such that
A193: y = [0,y9] and
A194: z = [0,z9] and
A195: +(y,z) = [0,y9 + z9] by A190,Def1;
    +(z,y) in [:{0},REAL+:] by A195,Lm1;
    then not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
    then consider x9,yz9 being Element of REAL+ such that
A196: x = [0,x9] and
A197: +(y,z) = [0,yz9] & +(x,+(y,z)) = [0,x9 + yz9] by A195,A192,Def1,Lm1;
A198: not(z in REAL+ & +(x,y) in [:{0},REAL+:]) by A191,Th5,XBOOLE_0:3;
    ( not(x in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & x in [:{0}
    ,REAL+:]) by A189,A190,Th5,XBOOLE_0:3;
    then consider x99,y99 being Element of REAL+ such that
A199: x = [0,x99] and
A200: y = [0,y99] and
A201: +(x,y) = [0,x99 + y99] by A189,Def1;
A202: x9 = x99 by A199,A196,XTUPLE_0:1;
    +(x,y) in [:{0},REAL+:] by A201,Lm1;
    then not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by Th5,XBOOLE_0:3;
    then consider xy99,z99 being Element of REAL+ such that
A203: +(x,y) = [0,xy99] and
A204: z = [0,z99] and
A205: +(+(x,y),z) = [0,xy99 + z99] by A201,A198,Def1,Lm1;
A206: z9 = z99 by A194,A204,XTUPLE_0:1;
A207: y9 = y99 by A193,A200,XTUPLE_0:1;
    thus +(x,+(y,z)) = [0,z9 + y9 + x9] by A195,A197,XTUPLE_0:1
      .= [0,z99 + (y99 + x99)] by A206,A202,A207,ARYTM_2:6
      .= +(+(x,y),z) by A201,A203,A205,XTUPLE_0:1;
  end;
end;

theorem
  [*x,y*] in REAL implies y = 0
proof
  assume
A1: [*x,y*] in REAL;
  assume y <> 0;
  then [*x,y*] = (0,1) --> (x,y) by Def5;
  hence contradiction by A1,Th8;
end;

theorem
  for x,y being Element of REAL holds opp +(x,y) = +(opp x, opp y)
proof
  reconsider o = 0 as Element of REAL by Lm3;
  let x,y be Element of REAL;
  +(+(x,y),+(opp x, opp y)) = +(x,+(y,+(opp x, opp y))) by Th23
    .= +(x,+(opp x,+(y, opp y))) by Th23
    .= +(x,+(opp x,o)) by Def3
    .= +(x,opp x) by Th11
    .= 0 by Def3;
  hence thesis by Def3;
end;