:: The Quaternion Numbers
::  by Xiquan Liang and Fuguo Ge
::
:: Received November 14, 2006
:: Copyright (c) 2006-2012 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 NUMBERS, XBOOLE_0, FUNCT_2, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1,
      FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, ZFMISC_1, XCMPLX_0, ARYTM_0, XREAL_0,
      ARYTM_3, ARYTM_2, ARYTM_1, COMPLEX1, REAL_1, SQUARE_1, XXREAL_0,
      QUATERNI;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, NUMBERS, RELAT_1,
      FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, COMPLEX1, ARYTM_0, ZFMISC_1,
      ARYTM_2, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0, RELSET_1, SEQ_1;
 constructors ENUMSET1, FUNCT_4, ARYTM_1, ARYTM_0, REAL_1, SQUARE_1, COMPLEX1,
      SEQ_1, VALUED_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, FUNCT_4,
      NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, VALUED_0, RELSET_1;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions SQUARE_1, TARSKI, COMPLEX1, ARYTM_3, XCMPLX_0;
 theorems FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, ENUMSET1, FUNCT_4, XBOOLE_1,
      FUNCT_1, ZFMISC_1, RELSET_1, COMPLEX1, ARYTM_2, ARYTM_0, SQUARE_1,
      XREAL_0, CARD_1, XCMPLX_0, XREAL_1, ARYTM_3, ORDINAL3, ABSVALUE,
      SERIES_3, XTUPLE_0;

begin

reserve a,b,c,d,x,y,X,w,z,x1,x2,x3,x4 for set;
reserve A for non empty set;

definition
  func QUATERNION equals
  Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
  x.2 = 0 & x.3 = 0} \/ COMPLEX;
  coherence;
end;

definition
  let x be number;
  attr x is quaternion means
  :Def2:
  x in QUATERNION;
end;

registration
  cluster QUATERNION -> non empty;
  coherence;
end;

definition
  let x,y,w,z,a,b,c,d;
  func (x,y,w,z) --> (a,b,c,d) -> set equals
  ((x,y) --> (a,b)) +* ((w,z) --> (c,d));
  coherence;
end;

registration
  let x,y,w,z,a,b,c,d;
  cluster (x,y,w,z) --> (a,b,c,d) -> Function-like Relation-like;
  coherence;
end;

theorem Th1:
  dom (x,y,w,z) --> (a,b,c,d) = {x,y,w,z}
proof
  set f=(x,y) --> (a,b), g=(w,z) --> (c,d);
A1: dom f={x,y} by FUNCT_4:62;
  dom g={w,z} by FUNCT_4:62;
  then dom f \/ dom g = {x,y,w,z} by A1,ENUMSET1:5;
  hence thesis by FUNCT_4:def 1;
end;

theorem Th2:
  rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
proof
  set f=(x,y) --> (a,b),g=(w,z) --> (c,d),
  h=((x,y) --> (a,b)) +* ((w,z) --> (c,d));
A1: rng f c= {a,b} by FUNCT_4:62;
  rng g c= {c,d} by FUNCT_4:62;
  then rng f \/ rng g c= {a,b} \/ {c,d} by A1,XBOOLE_1:13;
  then
A2: rng f \/ rng g c= {a,b,c,d} by ENUMSET1:5;
  rng h c= rng f \/ rng g by FUNCT_4:17;
  hence thesis by A2,XBOOLE_1:1;
end;

Lm1: 0,1,2,3 are_mutually_different by ZFMISC_1:def 6;

theorem Th3:
  x,y,w,z are_mutually_different implies
  ((x,y,w,z) --> (a,b,c,d)).x=a & ((x,y,w,z) --> (a,b,c,d)).y=b &
  ((x,y,w,z) --> (a,b,c,d)).w=c & ((x,y,w,z) --> (a,b,c,d)).z=d
proof
  assume
A1: x,y,w,z are_mutually_different; then
A2: x<>w by ZFMISC_1:def 6;
A3: x<>z by A1,ZFMISC_1:def 6;
A4: y<>w by A1,ZFMISC_1:def 6;
A5: y<>z by A1,ZFMISC_1:def 6;
A6: x<>y by A1,ZFMISC_1:def 6;
A7: w<>z by A1,ZFMISC_1:def 6;
  set f=(x,y) --> (a,b),g=(w,z) --> (c,d);
A8: f.x=a by A6,FUNCT_4:63;
A9: f.y=b by FUNCT_4:63;
A10: g.w=c by A7,FUNCT_4:63;
A11: g.z=d by FUNCT_4:63;
A12: dom g = {w,z} by FUNCT_4:62; then
A13: not x in dom g by A2,A3,TARSKI:def 2;
A14: not y in dom g by A4,A5,A12,TARSKI:def 2;
A15: w in dom g by A12,TARSKI:def 2;
  z in dom g by A12,TARSKI:def 2;
  hence thesis by A8,A9,A10,A11,A13,A14,A15,FUNCT_4:11,13;
end;

Lm2: x,y,w,z are_mutually_different implies
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d))
proof
  set h=(x,y,w,z) --> (a,b,c,d);
  assume
A1: x,y,w,z are_mutually_different;
  let y1 be set;
  assume y1 in {a,b,c,d}; then
A2: y1=a or y1=b or y1=c or y1=d by ENUMSET1:def 2;
A3: dom h = {x,y,w,z} by Th1;
A4: h.x=y1 or h.y=y1 or h.w=y1 or h.z=y1 by A1,A2,Th3;
A5: x in dom h by A3,ENUMSET1:def 2;
A6: y in dom h by A3,ENUMSET1:def 2;
A7: w in dom h by A3,ENUMSET1:def 2;
  z in dom h by A3,ENUMSET1:def 2;
  hence thesis by A4,A5,A6,A7,FUNCT_1:def 3;
end;

theorem
  x,y,w,z are_mutually_different implies
  rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
proof
  set h=(x,y,w,z) --> (a,b,c,d);
  assume
A1: x,y,w,z are_mutually_different;
A2: rng h c= {a,b,c,d} by Th2;
  {a,b,c,d} c= rng h by A1,Lm2;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  {x1,x2,x3,x4} c= X iff x1 in X & x2 in X & x3 in X & x4 in X
proof
A1: x1 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A2: x2 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A3: x3 in {x1,x2,x3,x4} by ENUMSET1:def 2;
  x4 in {x1,x2,x3,x4} by ENUMSET1:def 2;
  hence {x1,x2,x3,x4} c= X implies x1 in X & x2 in X & x3 in X & x4 in X
    by A1,A2,A3;
  assume that
A4: x1 in X and
A5: x2 in X and
A6: x3 in X and
A7: x4 in X;
  let z;
  assume z in {x1,x2,x3,x4};
  hence thesis by A4,A5,A6,A7,ENUMSET1:def 2;
end;

definition
  let A,x,y,w,z;
  let a,b,c,d be Element of A;
  redefine func (x,y,w,z) --> (a,b,c,d) -> Function of {x,y,w,z},A;
  coherence
  proof
    set f=(x,y) --> (a,b),g=(w,z) --> (c,d),h = (x,y,w,z) --> (a,b,c,d);
A1: rng h c= rng f \/ rng g by FUNCT_4:17;
A2: dom h = {x,y,w,z} by Th1;
    rng h c= A by A1,XBOOLE_1:1;
    hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
  end;
end;

definition
  func <j> equals
  (0,1,2,3) --> (0,0,1,0);
  coherence;
  func <k> equals
  (0,1,2,3) --> (0,0,0,1);
  coherence;
end;

Lm3: <i> = [*0,1*] by ARYTM_0:def 5;

registration
  cluster <i> -> quaternion;
  coherence
  proof
    thus <i> in QUATERNION by Lm3,XBOOLE_0:def 3;
  end;
  cluster <j> -> quaternion;
  coherence
  proof
    set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A1: now
      assume <j> in X;
      then ex x being Element of Funcs(4,REAL) st <j> = x & x.2=0 & x.3=0;
      hence contradiction by Lm1,Th3;
    end;
    reconsider z=0,j=0,w=1,m=0 as Element of REAL;
    <j> = (0,1,2,3) --> (z,j,w,m);
    then <j> in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
    then <j> in Funcs(4,REAL) \ X by A1,XBOOLE_0:def 5;
    hence <j> in QUATERNION by XBOOLE_0:def 3;
  end;
  cluster <k> -> quaternion;
  coherence
  proof
    set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A2: now
      assume <k> in X;
      then ex x being Element of Funcs(4,REAL) st <k> = x & x.2=0 & x.3=0;
      hence contradiction by Lm1,Th3;
    end;
    reconsider z=0,j=0,w=0,m=1 as Element of REAL;
    <k> = (0,1,2,3) --> (z,j,w,m);
    then <k> in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
    then <k> in Funcs(4,REAL) \ X by A2,XBOOLE_0:def 5;
    hence <k> in QUATERNION by XBOOLE_0:def 3;
  end;
end;

registration
  cluster quaternion for number;
  existence
  proof
    take <k>;
    thus thesis;
  end;
end;

registration
  cluster -> quaternion for Element of QUATERNION;
  coherence by Def2;
end;

definition
  let x,y,w,z be real number;
  func [*x,y,w,z*] -> Element of QUATERNION means
  :Def6:
  ex x9, y9 being Element of REAL st
  x9 = x & y9 = y & it = [*x9,y9*] if w=0 & z=0
  otherwise it = (0,1,2,3) --> (x,y,w,z);
  consistency;
  existence
  proof
    reconsider x9 = x, y9 = y, w9 = w, z9 = z as Element of REAL
    by XREAL_0:def 1;
    thus w = 0 & z = 0 implies ex t being Element of QUATERNION st
    ex x9, y9 being Element of REAL st
    x9 = x & y9 = y & t = [*x9,y9*]
    proof
      assume that w = 0 and z = 0;
      set t = [*x9,y9*];
      reconsider t as Element of QUATERNION by XBOOLE_0:def 3;
      take t;
      take x9, y9;
      thus thesis;
    end;
    set e = (0,1,2,3) --> (x9,y9,w9,z9);
    thus w <> 0 or z <> 0 implies
    ex t being Element of QUATERNION st t = (0,1,2,3) --> (x,y,w,z)
    proof
      assume
A1:   w <> 0 or z <> 0;
A2:   e in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
      now
        assume e in {r where r is Element of Funcs(4,REAL): r.2=0 & r.3=0};
        then ex r being Element of Funcs(4,REAL) st e = r & r.2=0 & r.3=0;
        hence contradiction by A1,Lm1,Th3;
      end;
      then e in Funcs(4,REAL)
      \ { r where r is Element of Funcs(4,REAL): r.2=0 & r.3 = 0}
      by A2,XBOOLE_0:def 5;
      then reconsider e as Element of QUATERNION by XBOOLE_0:def 3;
      take e;
      thus thesis;
    end;
  end;
  uniqueness;
end;

Lm4: for x,y being Element of REAL holds [*x,y,0,0*] = [*x,y*]
proof
  let x,y be Element of REAL;
  ex x9, y9 being Element of REAL st ( x9 = x)&( y9 = y)&( [*x
  ,y,0,0*] = [*x9,y9*]) by Def6;
  hence thesis;
end;

theorem Th6:
  for a,b,c,d,e,i,j,k being set,
  g being Function st a<>b & c <>d & dom g = {a,b,c,d} &
  g.a = e & g.b = i & g.c = j & g.d=k holds g = (a,b,c,d) --> (e,i,j,k)
proof
  let a,b,c,d,e,i,j,k be set;
  let h be Function such that
A1: a<>b and
A2: c <>d and
A3: dom h = {a,b,c,d} and
A4: h.a = e and
A5: h.b = i and
A6: h.c = j and
A7: h.d=k;
  set f = (a,b) --> (e,i);
  set g = (c,d) --> (j,k);
A8: dom f = {a,b} by FUNCT_4:62;
A9: dom g = {c,d} by FUNCT_4:62;
  then
A10: dom h = dom f \/ dom g by A3,A8,ENUMSET1:5;
  now
    let x such that
A11: x in dom f \/ dom g;
    thus x in dom g implies h.x = g.x
    proof
      assume
A12:  x in dom g;
      per cases by A9,A12,TARSKI:def 2;
      suppose x=c;
        hence thesis by A2,A6,FUNCT_4:63;
      end;
      suppose x=d;
        hence thesis by A7,FUNCT_4:63;
      end;
    end;
    thus not x in dom g implies h.x = f.x
    proof
      assume not x in dom g;
      then
A13:  x in dom f by A11,XBOOLE_0:def 3;
      per cases by A8,A13,TARSKI:def 2;
      suppose x=a;
        hence thesis by A1,A4,FUNCT_4:63;
      end;
      suppose x=b;
        hence thesis by A5,FUNCT_4:63;
      end;
    end;
  end;
  hence thesis by A10,FUNCT_4:def 1;
end;

theorem Th7:
  for g being quaternion number
  ex r,s,t,u being Element of REAL st g = [*r,s,t,u*]
proof
  let g be quaternion number;
A1:g in QUATERNION by Def2;
  per cases;
  suppose g in COMPLEX;
    then consider r,s being Element of REAL such that
A2: g = [*r,s*] by ARYTM_0:9;
    take r,s,0,0;
    thus thesis by A2,Def6,A1;
  end;
  suppose not g in COMPLEX;
    then
A3: g in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2=0 & x.3=0} by A1,XBOOLE_0:def 3;
    then consider f being Function such that
A4: g = f and
A5: dom f = 4 and
A6: rng f c= REAL by FUNCT_2:def 2;
A7: 0 in 4 by CARD_1:52,ENUMSET1:def 2;
A8: 1 in 4 by CARD_1:52,ENUMSET1:def 2;
A9: 2 in 4 by CARD_1:52,ENUMSET1:def 2;
A10: 3 in 4 by CARD_1:52,ENUMSET1:def 2;
A11: f.0 in rng f by A5,A7,FUNCT_1:3;
A12: f.1 in rng f by A5,A8,FUNCT_1:3;
A13: f.2 in rng f by A5,A9,FUNCT_1:3;
    f.3 in rng f by A5,A10,FUNCT_1:3;
    then reconsider
    r = f.0, s = f.1, t=f.2, u=f.3 as Element of REAL by A6,A11,A12,A13;
A14: g = (0,1,2,3)-->(r,s,t,u) by A4,A5,Th6,CARD_1:52;
    take r,s,t,u;
    now
      assume that
A15:  t=0 and
A16:  u=0;
A17:  (0,1,2,3)-->(r,s,t,u).2 = 0 by A15,Lm1,Th3;
      (0,1,2,3)-->(r,s,t,u).3 = 0 by A16,Lm1,Th3;
      then g in { x where x is Element of Funcs(4,REAL):
      x.2=0 & x.3=0} by A3,A14,A17;
      hence contradiction by A3,XBOOLE_0:def 5;
    end;
    hence thesis by A14,Def6;
  end;
end;

theorem Th8:
  a,c,x,w are_mutually_different
  implies (a,c,x,w) --> (b,d,y,z) = { [a,b], [c,d],[x,y],[w,z] }
proof
  assume
A1: a,c,x,w are_mutually_different;
  then
A2: a <> c by ZFMISC_1:def 6;
A3: a <> x by A1,ZFMISC_1:def 6;
A4: a <> w by A1,ZFMISC_1:def 6;
A5: c <> x by A1,ZFMISC_1:def 6;
A6: c <> w by A1,ZFMISC_1:def 6;
A7: x<>w by A1,ZFMISC_1:def 6;
  set m=(a,c) --> (b,d), n = (x,w) --> (y,z);
A8: dom m = {a,c} by FUNCT_4:62;
A9: dom n = {x,w} by FUNCT_4:62;
A10: not a in {x,w} by A3,A4,TARSKI:def 2;
  not c in {x,w} by A5,A6,TARSKI:def 2;
  then (a,c,x,w) --> (b,d,y,z) = m \/ n by A8,A9,A10,FUNCT_4:31,ZFMISC_1:51
    .={ [a,b], [c,d] } \/ n by A2,FUNCT_4:67
    .={ [a,b], [c,d] } \/ {[x,y],[w,z]} by A7,FUNCT_4:67
    .={ [a,b], [c,d], [x,y],[w,z]} by ENUMSET1:5;
  hence thesis;
end;

reserve i,j,k for Element of NAT;
reserve a,b,c,d for Element of REAL;
reserve y,r,s,x,t,w for Element of RAT+;

Lm5: 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
A2: {x,y} in {z} by TARSKI:def 2;
  {x} in {z} by A1,TARSKI:def 2;
  hence
A3: z = {x} by TARSKI:def 1;
  {x,y} = z by A2,TARSKI:def 1;
  hence thesis by A3,ZFMISC_1:5;
end;

theorem Th9:
  for A being Subset of RAT+ st (ex t st t in A & t <> {}) &
  for r,s st r in A & s <=' r holds s in A
  ex r1,r2,r3,r4,r5 being Element of RAT+ st
  r1 in A & r2 in A & r3 in A & r4 in A & r5 in A &
  r1 <> r2 & r1 <> r3 & r1<>r4 & r1 <> r5 & r2<> r3 & r2<> r4 &
  r2<> r5& r3 <> r4 & r3 <> r5 & r4 <> r5
proof
  let A be Subset of RAT+;
  given t such that
A1: t in A and
A2: t <> {};
  assume
A3: for r,s st r in A & s <=' r holds s in A;
  consider x such that
A4: t = x+x by ARYTM_3:60;
  consider y such that
A5: x = y+y by ARYTM_3:60;
  consider w such that
A6: y = w+w by ARYTM_3:60;
  take {},w,y,x,t;
A7: {} <=' t by ARYTM_3:64;
A8: x <=' t by A4,ARYTM_3:def 13;
A9: y <=' x by A5,ARYTM_3:def 13;
A10: w<=' y by A6,ARYTM_3:def 13;
A11: y <=' t by A8,A9,ARYTM_3:67;
  w <=' x by A9,A10,ARYTM_3:67;
  hence {} in A & w in A & y in A & x in A & t in A by A1,A3,A7,A8,A9,
ARYTM_3:67;
A12: {} <> x by A2,A4,ARYTM_3:50;
  then
A13: {} <> y by A5,ARYTM_3:50;
A14: x <> t
  proof
    assume x = t;
    then t+{} = t+t by A4,ARYTM_3:50;
    hence contradiction by A2,ARYTM_3:62;
  end;
A15: y <> x
  proof
    assume y = x;
    then x+{} = x+x by A5,ARYTM_3:50;
    hence contradiction by A12,ARYTM_3:62;
  end;
  w <> y
  proof
    assume w = y;
    then y+{} = y+y by A6,ARYTM_3:50;
    hence contradiction by A13,ARYTM_3:62;
  end;
  hence thesis by A2,A4,A5,A6,A8,A9,A10,A11,A14,A15,ARYTM_3:50,66;
end;

Lm6: not (0,1,2,3) --> (a,b,c,d) in REAL
proof
  set f = (0,1,2,3)-->(a,b,c,d);
A1: f = { [0,a], [1,b],[2,c],[3,d]} by Lm1,Th8;
  now
    assume f in {[i,j]: i,j are_relative_prime & j <> {}};
    then consider i,j such that
A2: f = [i,j] and i,j are_relative_prime and j<> {};
A3: {i} in f by A2,TARSKI:def 2;
A4: {i,j} in f by A2,TARSKI:def 2;
A5: now
      assume i = j;
      then {i} = {i,j} by ENUMSET1:29;
      then
A6:   [i,j] = {{i}} by ENUMSET1:29;
      then
A7:   [0,a] in {{i}} by A1,A2,ENUMSET1:def 2;
A8:   [1,b] in {{i}} by A1,A2,A6,ENUMSET1:def 2;
A9:   [0,a] = {i} by A7,TARSKI:def 1;
      [1,b] = {i} by A8,TARSKI:def 1;
      hence contradiction by A9,XTUPLE_0:1;
    end;
    per cases by A1,A3,A4,ENUMSET1:def 2;
    suppose {i} = [0,a] & {i,j} = [0,a];
      hence contradiction by A5,ZFMISC_1:5;
    end;
    suppose that
A10:  {i} = [0,a] and
A11:  {i,j} = [1,b];
A12:  i = {0} by A10,Lm5;
      i in [1,b] by A11,TARSKI:def 2;
      then i = {1,b} or i = {1} by TARSKI:def 2;
      then 1 in i by TARSKI:def 1,def 2;
      hence contradiction by A12,TARSKI:def 1;
    end;
    suppose that
A13:  {i} = [0,a] and
A14:  {i,j} = [2,c];
A15:  i = {0} by A13,Lm5;
      i in [2,c] by A14,TARSKI:def 2;
      then i = {2,c} or i = {2} by TARSKI:def 2;
      then 2 in i by TARSKI:def 1,def 2;
      hence contradiction by A15,TARSKI:def 1;
    end;
    suppose that
A16:  {i} = [0,a] and
A17:  {i,j} = [3,d];
A18:  i = {0} by A16,Lm5;
      i in [3,d] by A17,TARSKI:def 2;
      then i = {3,d} or i = {3} by TARSKI:def 2;
      then 3 in i by TARSKI:def 1,def 2;
      hence contradiction by A18,TARSKI:def 1;
    end;
    suppose that
A19:  {i} = [1,b] and
A20:  {i,j} = [0,a];
A21:  i = {1} by A19,Lm5;
      i in [0,a] by A20,TARSKI:def 2;
      then i = {0,a} or i = {0} by TARSKI:def 2;
      then 0 in i by TARSKI:def 1,def 2;
      hence contradiction by A21,TARSKI:def 1;
    end;
    suppose {i} = [1,b] & {i,j} = [1,b];
      hence contradiction by A5,ZFMISC_1:5;
    end;
    suppose that
A22:  {i} = [1,b] and
A23:  {i,j} = [2,c];
A24:  i = {1} by A22,Lm5;
      i in [2,c] by A23,TARSKI:def 2;
      then i = {2,c} or i = {2} by TARSKI:def 2;
      then 2 in i by TARSKI:def 1,def 2;
      hence contradiction by A24,TARSKI:def 1;
    end;
    suppose that
A25:  {i} = [1,b] and
A26:  {i,j} = [3,d];
A27:  i = {1} by A25,Lm5;
      i in [3,d] by A26,TARSKI:def 2;
      then i = {3,d} or i = {3} by TARSKI:def 2;
      then 3 in i by TARSKI:def 1,def 2;
      hence contradiction by A27,TARSKI:def 1;
    end;
    suppose that
A28:  {i} = [2,c] and
A29:  {i,j} = [0,a];
A30:  i = {2} by A28,Lm5;
      i in [0,a] by A29,TARSKI:def 2;
      then i = {0,a} or i = {0} by TARSKI:def 2;
      then 0 in i by TARSKI:def 1,def 2;
      hence contradiction by A30,TARSKI:def 1;
    end;
    suppose that
A31:  {i} = [2,c] and
A32:  {i,j} = [1,b];
A33:  i = {2} by A31,Lm5;
      i in [1,b] by A32,TARSKI:def 2;
      then i = {1,b} or i = {1} by TARSKI:def 2;
      then 1 in i by TARSKI:def 1,def 2;
      hence contradiction by A33,TARSKI:def 1;
    end;
    suppose {i} = [2,c] & {i,j} = [2,c];
      hence contradiction by A5,ZFMISC_1:5;
    end;
    suppose that
A34:  {i} = [2,c] and
A35:  {i,j} = [3,d];
A36:  i = {2} by A34,Lm5;
      i in [3,d] by A35,TARSKI:def 2;
      then i = {3,d} or i = {3} by TARSKI:def 2;
      then 3 in i by TARSKI:def 1,def 2;
      hence contradiction by A36,TARSKI:def 1;
    end;
    suppose that
A37:  {i} = [3,d] and
A38:  {i,j} = [0,a];
A39:  i = {3} by A37,Lm5;
      i in [0,a] by A38,TARSKI:def 2;
      then i = {0,a} or i = {0} by TARSKI:def 2;
      then 0 in i by TARSKI:def 1,def 2;
      hence contradiction by A39,TARSKI:def 1;
    end;
    suppose that
A40:  {i} = [3,d] and
A41:  {i,j} = [1,b];
A42:  i = {3} by A40,Lm5;
      i in [1,b] by A41,TARSKI:def 2;
      then i = {1,b} or i = {1} by TARSKI:def 2;
      then 1 in i by TARSKI:def 1,def 2;
      hence contradiction by A42,TARSKI:def 1;
    end;
    suppose that
A43:  {i} = [3,d] and
A44:  {i,j} = [2,c];
A45:  i = {3} by A43,Lm5;
      i in [2,c] by A44,TARSKI:def 2;
      then i = {2,c} or i = {2} by TARSKI:def 2;
      then 2 in i by TARSKI:def 1,def 2;
      hence contradiction by A45,TARSKI:def 1;
    end;
    suppose {i} = [3,d] & {i,j} = [3,d];
      hence contradiction by A5,ZFMISC_1:5;
    end;
  end;
  then
A46: not f in {[i,j]: i,j are_relative_prime & j <> {}} \
  {[k,1]: not contradiction};
  now
    assume f in omega;
    then {} in f by ORDINAL3:8;
    hence contradiction by A1,ENUMSET1:def 2;
  end;
  then
A47: not f in RAT+ by A46,XBOOLE_0:def 3;
  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};
  not ex x,y,z,w being set st {[0,x],[1,y],[2,z],[3,w]} in IR
  proof
    given x,y,z,w being set such that
A48: {[0,x],[1,y],[2,z],[3,w]} in IR;
    consider A being Subset of RAT+ such that
A49: {[0,x],[1,y],[2,z],[3,w]} = A and
A50: 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 A48;
A51: [0,x] in A by A49,ENUMSET1:def 2;
    for r,s being Element of RAT+ st r in A & s <=' r holds s in A by A50;
    then consider r1,r2,r3,r4,r5 being Element of RAT+ such that
A52: r1 in A and
A53: r2 in A and
A54: r3 in A and
A55: r4 in A and
A56: r5 in A and
A57: r1 <> r2 and
A58: r1 <> r3 and
A59: r1<>r4 and
A60: r1 <> r5 and
A61: r2<> r3 and
A62: r2<> r4 and
A63: r2<> r5 and
A64: r3 <> r4 and
A65: r3 <> r5 and
A66: r4 <> r5 by A51,Th9;
A67: r1 = [0,x] or r1 = [1,y] or r1 = [2,z] or r1 = [3,w] by A49,A52,
ENUMSET1:def 2;
A68: r2 = [0,x] or r2 = [1,y] or r2 = [2,z] or r2 = [3,w] by A49,A53,
ENUMSET1:def 2;
A69: r3 = [0,x] or r3 = [1,y] or r3 = [2,z] or r3 = [3,w] by A49,A54,
ENUMSET1:def 2;
    r4 = [0,x] or r4 = [1,y] or r4 = [2,z] or r4 = [3,w] by A49,A55,
ENUMSET1:def 2;
    hence contradiction by A49,A56,A57,A58,A59,A60,A61,A62,A63,A64,A65,A66,A67
,A68,A69,ENUMSET1:def 2;
  end;
  then not f in DEDEKIND_CUTS by A1,ARYTM_2:def 1;
  then
A70: not f in REAL+ by A47,ARYTM_2:def 2,XBOOLE_0:def 3;
  now
    assume f in [:{{}},REAL+:];
    then consider x,y being set such that
A71: x in {{}} and y in REAL+ and
A72: f = [x,y] by ZFMISC_1:84;
A73: x = 0 by A71,TARSKI:def 1;
    f = {[0,a],[1,b],[2,c],[3,d]} by Lm1,Th8;
    then
A74: [1,b] in f by ENUMSET1:def 2;
    per cases by A72,A73,A74,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;
  hence thesis by A70,NUMBERS:def 1,XBOOLE_0:def 3;
end;

theorem Th10:
  not (0,1,2,3) --> (a,b,c,d) in COMPLEX
proof
  set f = (0,1,2,3)-->(a,b,c,d);
A1: not f in REAL by Lm6;
  not f in Funcs({0,1},REAL)
  proof
    assume f in Funcs({0,1},REAL);
    then dom f = {0,1} by FUNCT_2:92;
    then {0,1,2,3} c= {0,1} by Th1;
    then {0,1} \/ {2,3} c= {0,1} by ENUMSET1:5;
    hence contradiction by XBOOLE_1:11,ZFMISC_1:22;
  end;
  then not f in Funcs({0,1},REAL)\
  { x where x is Element of Funcs({0,1},REAL): x.1 = 0};
  hence thesis by A1,NUMBERS:def 2,XBOOLE_0:def 3;
end;

theorem Th11:
  for a,b,c,d,x,y,z,w,x9,y9,z9,w9 being set st a,b,c,d are_mutually_different &
  (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9)
  holds x = x9 & y = y9 & z=z9 & w=w9
proof
  let a,b,c,d,x,y,z,w,x9,y9,z9,w9 be set such that
A1: a,b,c,d are_mutually_different and
A2: (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9);
A3: x=((a,b,c,d) --> (x,y,z,w)).a by A1,Th3
    .=x9 by A1,A2,Th3;
A4: y=((a,b,c,d) --> (x,y,z,w)).b by A1,Th3
    .=y9 by A1,A2,Th3;
A5: z=((a,b,c,d) --> (x,y,z,w)).c by A1,Th3
    .=z9 by A1,A2,Th3;
  w=((a,b,c,d) --> (x,y,z,w)).d by A1,Th3
    .=w9 by A1,A2,Th3;
  hence thesis by A3,A4,A5;
end;

theorem Th12:
  for x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL st [*x1,x2,x3,x4*]
  = [*y1,y2,y3,y4*] holds x1 = y1 & x2 = y2 & x3=y3 & x4=y4
proof
  let x1,x2,x3,x4,y1,y2,y3,y4 be Element of REAL such that
A1: [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*];
  per cases;
  suppose
A2: x3=0 & x4=0;
    then
A3: [*x1,x2,x3,x4*] = [*x1,x2*] by Lm4;
A4: now
      assume y3<>0 or y4<>0;
      then [*x1,x2*] = (0,1,2,3) --> (y1,y2,y3,y4) by A1,A3,Def6;
      hence contradiction by Th10;
    end;
    then [*y1,y2,y3,y4*] = [*y1,y2*] by Lm4;
    hence thesis by A1,A2,A3,A4,ARYTM_0:10;
  end;
  suppose x3<>0 or x4<>0;
    then
A5: [*y1,y2,y3,y4*] = (0,1,2,3) --> (x1,x2,x3,x4) by A1,Def6;
    now
      assume that
A6:   y3=0 and
A7:   y4=0;
      [*y1,y2,y3,y4*] = [*y1,y2*] by A6,A7,Lm4;
      hence contradiction by A5,Th10;
    end;
    then [*y1,y2,y3,y4*] = (0,1,2,3) --> (y1,y2,y3,y4) by Def6;
    hence thesis by A5,Lm1,Th11;
  end;
end;

definition
  let x,y be quaternion number;
  consider x1,x2,x3,x4 being Element of REAL such that
A1: x = [*x1,x2,x3,x4*] by Th7;
  consider y1,y2,y3,y4 being Element of REAL such that
A2: y = [*y1,y2,y3,y4*] by Th7;
  func x + y means
  :Def7:
  ex x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL st
  x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] &
  it = [*x1+y1,x2+y2,x3+y3,x4+y4*];
  existence
  proof
    take [*x1+y1,x2+y2,x3+y3,x4+y4*];
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let c1,c2 be number;
    given x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A3: x = [*x1,x2,x3,x4*] and
A4: y = [*y1,y2,y3,y4*] and
A5: c1 = [*x1+y1,x2+y2,x3+y3,x4+y4*];
    given x19,x29,x39,x49,y19,y29,y39,y49 being Element of REAL such that
A6: x = [*x19,x29,x39,x49*] and
A7: y = [*y19,y29,y39,y49*] and
A8: c2 = [*x19+y19,x29+y29,x39+y39,x49+y49*];
A9: x1 = x19 by A3,A6,Th12;
A10: x2 = x29 by A3,A6,Th12;
A11: x3=x39 by A3,A6,Th12;
A12: x4=x49 by A3,A6,Th12;
A13: y1 = y19 by A4,A7,Th12;
A14: y2 = y29 by A4,A7,Th12;
    y3=y39 by A4,A7,Th12;
    hence thesis by A4,A5,A7,A8,A9,A10,A11,A12,A13,A14,Th12;
  end;
  commutativity;
end;

Lm7: 0 = [*0,0,0,0*]
proof
  ex x9, y9 being Element of REAL st ( x9 = 0)&( y9 = 0)&( [*0
  ,0,0,0*] = [*x9,y9*]) by Def6;
  hence thesis by ARYTM_0:def 5;
end;

definition
  let z be quaternion number;
  consider v,w,x,y being Element of REAL such that
A1: z = [*v,w,x,y*] by Th7;
  func - z -> quaternion number means
  :Def8:
  z + it = 0;
  existence
  proof
    reconsider z9 = [*- v, - w, - x, - y*] as quaternion number;
    take z9;
A2: 0 =v+ -v;
A3: 0 = w+ -w;
A4: 0 = x+ -x;
    0 = y+ -y;
    hence thesis by A1,A2,A3,A4,Def7,Lm7;
  end;
  uniqueness
  proof
    let c1,c2 be quaternion number such that
A5: z + c1 = 0 and
A6: z + c2 = 0;
    consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A7: z = [*x1,x2,x3,x4*] and
A8: c1 = [*y1,y2,y3,y4*] and
A9: 0 = [*x1+y1,x2+y2,x3+y3,x4+y4*] by A5,Def7;
    consider x19,x29,x39,x49,y19,y29,y39,y49 being Element of REAL such that
A10: z = [*x19,x29,x39,x49*] and
A11: c2 = [*y19,y29,y39,y49*] and
A12: 0 = [*x19+y19,x29+y29,x39+y39,x49+y49*] by A6,Def7;
A13: x1 = x19 by A7,A10,Th12;
A14: x2 = x29 by A7,A10,Th12;
A15: x3 = x39 by A7,A10,Th12;
A16: x4 = x49 by A7,A10,Th12;
A17: x1+y1 = 0 by A9,Lm7,Th12;
A18: x1+y19 = 0 by A12,A13,Lm7,Th12;
A19: x2+y2 = 0 by A9,Lm7,Th12;
A20: x2+y29 = 0 by A12,A14,Lm7,Th12;
A21: x3+y3 = 0 by A9,Lm7,Th12;
A22: x3+y39 = 0 by A12,A15,Lm7,Th12;
A23: x4+y4 = 0 by A9,Lm7,Th12;
    x4+y49 = 0 by A12,A16,Lm7,Th12;
    hence thesis by A8,A11,A17,A18,A19,A20,A21,A22,A23;
  end;
  involutiveness;
end;

definition
  let x,y be quaternion number;
  func x-y equals
  x + - y;
  coherence;
end;

definition
  let x,y be quaternion number;
  consider x1,x2,x3,x4 being Element of REAL such that
A1: x = [*x1,x2,x3,x4*] by Th7;
  consider y1,y2,y3,y4 being Element of REAL such that
A2: y = [*y1,y2,y3,y4*] by Th7;
  func x*y means
  :Def10:
  ex x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL st
  x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [* x1*y1-x2*y2-x3*y3-x4*y4,
  x1*y2+x2*y1+x3*y4-x4*y3, x1*y3+y1*x3+y2*x4-y4*x2,
  x1*y4+x4*y1+x2*y3-x3*y2 *];
  existence
  proof
    take [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
    x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *];
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let c1,c2 be number;
    given x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A3: x = [*x1,x2,x3,x4*] and
A4: y = [*y1,y2,y3,y4*] and
A5: c1 = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
    x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *];
    given x19,x29,x39,x49,y19,y29,y39,y49 being Element of REAL such that
A6: x = [*x19,x29,x39,x49*] and
A7: y = [*y19,y29,y39,y49*] and
A8: c2 = [* x19*y19-x29*y29-x39*y39-x49*y49, x19*y29+x29*y19+x39*y49-x49*y39,
    x19*y39+y19*x39+y29*x49-y49*x29, x19*y49+x49*y19+x29*y39-x39*y29 *];
A9: x1 = x19 by A3,A6,Th12;
A10: x2 = x29 by A3,A6,Th12;
A11: x3 = x39 by A3,A6,Th12;
A12: x4 = x49 by A3,A6,Th12;
A13: y1 = y19 by A4,A7,Th12;
A14: y2 = y29 by A4,A7,Th12;
A15: y3 = y39 by A4,A7,Th12;
    y4 = y49 by A4,A7,Th12;
    hence thesis by A5,A8,A9,A10,A11,A12,A13,A14,A15;
  end;
end;

registration
  let z,z9 be quaternion number;
  cluster z + z9 -> quaternion;
  coherence
  proof
    ex x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL st
    z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] &
    z + z9 = [*x1+y1,x2+y2,x3+y3,x4+y4*] by Def7;
    hence thesis;
  end;
  cluster z*z9 -> quaternion;
  coherence
  proof
    ex x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL st
    z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] &
    z*z9 = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
    x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *] by Def10;
    hence z*z9 in QUATERNION;
  end;
end;

definition
  redefine func <j> -> Element of QUATERNION equals
  [*0,0,1,0*];
  coherence by Def2;
  compatibility by Def6;
  redefine func <k> -> Element of QUATERNION equals
  [*0,0,0,1*];
  coherence by Def2;
  compatibility by Def6;
end;

theorem
  <i> * <i> = -1
proof
  <i> = [*0,1,0,0*] by Lm3,Lm4; then
A1: <i> * <i> = [* 0*0-1*1-0*0-0*0, 0*1+1*0+0*0-0*0,
  0*0+0*0+1*0-0*1, 0*0+0*0+1*0-0*1 *] by Def10
    .= [*-1,0,0,0*];
  -1 = [*-1,0*] by ARYTM_0:def 5;
  hence thesis by A1,Lm4;
end;

theorem
  <j> * <j> = -1
proof
A1: <j> * <j> = [* 0*0-0*0-1*1-0*0, 0*0+0*0+0*0-0*1,
  0*1+0*1+0*0-0*0, 0*0+0*0+0*1-1*0 *] by Def10
    .= [*-1,0,0,0*];
  [*-1,0,0,0*] = [*-1,0*] by Lm4;
  hence thesis by A1,ARYTM_0:def 5;
end;

theorem
  <k> * <k> = -1
proof
A1: <k> * <k> = [* 0*0-0*0-0*0-1*1, 0*0+0*0+0*1-1*0,
  0*0+0*0+0*1-1*0, 0*1+1*0+0*0-0*0 *] by Def10
    .= [*-1,0,0,0*];
  -1 = [*-1,0*] by ARYTM_0:def 5;
  hence thesis by A1,Lm4;
end;

theorem
  <i> * <j> = <k>
proof
  <i> = [*0,1,0,0*] by Lm3,Lm4;
  then <i> * <j> = [* 0*0-1*0-0*1-0*0, 0*0+1*0+0*0-0*1,
  0*1+0*0+0*0-0*1, 0*0+0*0+1*1-0*0 *] by Def10
    .= [*0,0,0,1*];
  hence thesis;
end;

theorem
  <j> * <k> = <i>
proof
  <j> * <k> = [* 0*0-0*0-1*0-0*1, 0*0+0*0+1*1-0*0,
  0*0+0*1+0*0-1*0, 0*1+0*0+0*0-1*0 *] by Def10
    .= [*0,1,0,0*];
  hence thesis by Lm3,Lm4;
end;

theorem
  <k> * <i> = <j>
proof
  <i> = [*0,1,0,0*] by Lm3,Lm4;
  then <k> * <i> = [* 0*0-0*1-0*0-1*0, 0*1+0*0+0*0-1*0,
  0*0+0*0+1*1-0*0, 0*0+1*0+0*0-0*1 *] by Def10
    .= [*0,0,1,0*];
  hence thesis;
end;

theorem
  <i> * <j> = - <j> * <i>
proof
A1: <i> = [*0,1,0,0*] by Lm3,Lm4;
  then
A2: <i> * <j> = [* 0*0-1*0-0*1-0*0, 0*0+1*0+0*0-0*1,
  0*1+0*0+0*0-0*1, 0*0+0*0+1*1-0*0 *] by Def10
    .= [*0,0,0,1*];
  <j> * <i> = [* 0*0-0*1-1*0-0*0, 0*1+0*0+1*0-0*0,
  0*0+0*1+1*0-0*0, 0*0+0*0+0*0-1*1 *] by A1,Def10
    .= [*0,0,0,-1*];
  then <i> * <j> + <j> * <i> = [*0+0,0+0,0+0,1+ -1*] by A2,Def7
    .= 0 by Lm7;
  hence thesis by Def8;
end;

theorem
  <j> * <k> = - <k> * <j>
proof
A1: <j> * <k> = [* 0*0-0*0-1*0-0*1, 0*0+0*0+1*1-0*0,
  0*0+0*1+0*0-1*0, 0*1+0*0+0*0-1*0 *] by Def10
    .= [*0,1,0,0*];
  <k> * <j> = [* 0*0-0*0-0*1-1*0, 0*0+0*0+0*0-1*1,
  0*1+0*0+0*1-0*0, 0*0+1*0+0*1-0*0 *] by Def10
    .= [*0,-1,0,0*];
  then <j> * <k> + <k> * <j> = [*0+0,0+0,0+0,1+ -1*] by A1,Def7
    .= 0 by Lm7;
  hence thesis by Def8;
end;

theorem
  <k> * <i> = - <i> * <k>
proof
A1: <i> = [*0,1,0,0*] by Lm3,Lm4;
  then
A2: <k> * <i> = [* 0*0-0*1-0*0-1*0, 0*1+0*0+0*0-1*0,
  0*0+0*0+1*1-0*0, 0*0+1*0+0*0-0*1 *] by Def10
    .= [*0,0,1,0*];
  <i> * <k> = [* 0*0-1*0-0*0-0*1, 0*0+1*0+0*1-0*0,
  0*0+0*0+0*1-1*1, 0*1+0*0+1*0-0*0 *] by A1,Def10
    .= [*0,0,-1,0*];
  then <k> * <i> + <i> * <k> = [*0+0,0+0,1+ -1,0+0*] by A2,Def7
    .= 0 by Lm7;
  hence thesis by Def8;
end;

definition
  let z be quaternion number;
  func Rea z means
  :Def13:
  ex z9 being complex number st z=z9 & it = Re z9 if z in COMPLEX otherwise
  ex f being Function of 4,REAL st z = f & it = f.0;
  existence
  proof
    thus z in COMPLEX implies ex IT being set,
    z9 being complex number st z=z9 & IT = Re z9
    proof
      assume z in COMPLEX;
      then consider r,s being Element of REAL such that
A1:   z = [*r,s*] by ARYTM_0:9;
      set z9=[*r,s*];
      take Re z9,z9;
      thus thesis by A1;
    end;
    assume
A2: not z in COMPLEX;
    z in QUATERNION by Def2;
    then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2=0 & x.3=0} by A2,XBOOLE_0:def 3;
    then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
    take f.0, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
  func Im1 z means
  :Def14:
  ex z9 being complex number st z=z9 & it = Im z9 if z in COMPLEX otherwise
  ex f being Function of 4,REAL st z = f & it = f.1;
  existence
  proof
    thus z in COMPLEX implies ex IT being set,
    z9 being complex number st z=z9 & IT = Im z9
    proof
      assume z in COMPLEX;
      then consider r,s being Element of REAL such that
A3:   z = [*r,s*] by ARYTM_0:9;
      set z9=[*r,s*];
      take Im z9,z9;
      thus thesis by A3;
    end;
    assume
A4: not z in COMPLEX;
    z in QUATERNION by Def2;
    then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2=0 & x.3=0} by A4,XBOOLE_0:def 3;
    then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
    take f.1, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
  func Im2 z means
  :Def15:
  it = 0 if z in COMPLEX otherwise
  ex f being Function of 4,REAL st z = f & it = f.2;
  existence
  proof
    thus z in COMPLEX implies ex IT being set st IT = 0;
    assume
A5: not z in COMPLEX;
    z in QUATERNION by Def2;
    then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2=0 & x.3=0} by A5,XBOOLE_0:def 3;
    then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
    take f.2, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
  func Im3 z means
  :Def16:
  it = 0 if z in COMPLEX otherwise
  ex f being Function of 4,REAL st z = f & it = f.3;
  existence
  proof
    thus z in COMPLEX implies ex IT being set st IT = 0;
    assume
A6: not z in COMPLEX;
    z in QUATERNION by Def2;
    then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2=0 & x.3=0} by A6,XBOOLE_0:def 3;
    then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
    take f.3, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
end;

registration
  let z be quaternion number;
  cluster Rea z -> real;
  coherence
  proof
    per cases;
    suppose z in COMPLEX;
      then ex z9 being complex number st ( z = z9)&( Rea z = Re z9) by Def13;
      hence thesis;
    end;
    suppose not z in COMPLEX;
      then ex f being Function of 4,REAL st ( z = f)&( Rea z = f.0) by Def13;
      hence thesis;
    end;
  end;
  cluster Im1 z -> real;
  coherence
  proof
    per cases;
    suppose z in COMPLEX;
      then ex z9 being complex number st ( z = z9)&( Im1 z = Im z9) by Def14;
      hence thesis;
    end;
    suppose not z in COMPLEX;
      then ex f being Function of 4,REAL st ( z = f)&( Im1 z = f.1) by Def14;
      hence thesis;
    end;
  end;
  cluster Im2 z -> real;
  coherence
  proof
    per cases;
    suppose z in COMPLEX;
      hence thesis by Def15;
    end;
    suppose not z in COMPLEX;
      then ex f being Function of 4,REAL st ( z = f)&( Im2 z = f.2) by Def15;
      hence thesis;
    end;
  end;
  cluster Im3 z -> real;
  coherence
  proof
    per cases;
    suppose z in COMPLEX;
      hence thesis by Def16;
    end;
    suppose not z in COMPLEX;
      then ex f being Function of 4,REAL st ( z = f)&( Im3 z = f.3) by Def16;
      hence thesis;
    end;
  end;
end;

definition
  let z be quaternion number;
  redefine func Rea z -> Real;
  coherence by XREAL_0:def 1;
  redefine func Im1 z -> Real;
  coherence by XREAL_0:def 1;
  redefine func Im2 z -> Real;
  coherence by XREAL_0:def 1;
  redefine func Im3 z -> Real;
  coherence by XREAL_0:def 1;
end;

theorem Th22:
  for f being Function of 4,REAL ex a,b,c,d st f = (0,1,2,3)-->(a,b,c,d)
proof
  let f be Function of 4,REAL;
  reconsider a = f.0, b = f.1, c = f.2, d = f.3 as Element of REAL;
  take a,b,c,d;
  dom f = {0,1,2,3} by CARD_1:52,FUNCT_2:def 1;
  hence thesis by Th6;
end;

Lm8: Re [*a,b*] = a & Im [*a,b*] = b
proof
  reconsider a9 =a, b9 = b as Element of REAL;
  thus Re [*a,b*] = a proof per cases;
    suppose b = 0;
      then [*a,b*] = a by ARYTM_0:def 5;
      hence thesis by COMPLEX1:def 1;
    end;
    suppose b <> 0;
      then
A1:   [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
      then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
A2:   not [*a,b*] in REAL by A1,ARYTM_0:8;
      f.0 = a by A1,FUNCT_4:63;
      hence thesis by A2,COMPLEX1:def 1;
    end;
  end;
  per cases;
  suppose
A3: b = 0;
    then [*a,b*] = a by ARYTM_0:def 5;
    hence thesis by A3,COMPLEX1:def 2;
  end;
  suppose b <> 0;
    then
A4: [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
    then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
A5: not [*a,b*] in REAL by A4,ARYTM_0:8;
    f.1 = b by A4,FUNCT_4:63;
    hence thesis by A5,COMPLEX1:def 2;
  end;
end;

Lm9: for z being complex number holds [*Re z, Im z*] = z
proof
  let z be complex number;
A1: z in COMPLEX by XCMPLX_0:def 2;
  per cases;
  suppose
A2: z in REAL;
    then Im z = 0 by COMPLEX1:def 2;
    hence [*Re z, Im z*] = Re z by ARYTM_0:def 5
      .= z by A2,COMPLEX1:def 1;
  end;
  suppose
A3: not z in REAL;
    then
A4: ex f being Function of 2,REAL st ( z = f)&( Im z = f.1) by COMPLEX1:def 2;
A5: ex f being Function of 2,REAL st ( z = f)&( Re z = f.0) by A3,
COMPLEX1:def 1;
    consider a,b such that
A6: z = (0,1)-->(a,b) by A4,COMPLEX1:2;
A7: Re z = a by A5,A6,FUNCT_4:63;
A8: Im z = b by A4,A6,FUNCT_4:63;
    z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0 }
    by A1,A3,CARD_1:50,NUMBERS:def 2,XBOOLE_0:def 3;
    then
A9: not z in { x where x is Element of Funcs(2,REAL): x.1 = 0}
    by XBOOLE_0:def 5;
    reconsider f = z as Element of Funcs(2,REAL) by A6,CARD_1:50,FUNCT_2:8;
    f.1 <> 0 by A9;
    then b <> 0 by A6,FUNCT_4:63;
    hence thesis by A6,A7,A8,ARYTM_0:def 5;
  end;
end;

theorem Th23:
  Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b &
  Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d
proof
  reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of REAL;
  thus Rea [*a,b,c,d*] = a
  proof
    per cases;
    suppose c = 0 & d=0;
      then
A1:   [*a,b,c,d*] = [*a,b*] by Lm4;
      Re [*a,b*] =a by Lm8;
      hence thesis by A1,Def13;
    end;
    suppose c <> 0 or d<>0;
      then
A2:   [*a,b,c,d*] = (0,1,2,3)-->(a9,b9,c9,d9) by Def6;
      then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A3:   not [*a,b,c,d*] in COMPLEX by A2,Th10;
      f.0 = a by A2,Lm1,Th3;
      hence thesis by A3,Def13;
    end;
  end;
  thus Im1 [*a,b,c,d*] = b
  proof
    per cases;
    suppose c = 0 & d = 0;
      then
A4:   [*a,b,c,d*] = [*a,b*] by Lm4;
      Im [*a,b*] = b by Lm8;
      hence thesis by A4,Def14;
    end;
    suppose c <> 0 or d <> 0;
      then
A5:   [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
      then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A6:   not [*a,b,c,d*] in COMPLEX by A5,Th10;
      f.1 = b by A5,Lm1,Th3;
      hence thesis by A6,Def14;
    end;
  end;
  thus Im2 [*a,b,c,d*] = c
  proof
    per cases;
    suppose
A7:   c = 0 & d = 0;
      then [*a,b,c,d*] = [*a,b*] by Lm4;
      hence thesis by A7,Def15;
    end;
    suppose c <> 0 or d <> 0;
      then
A8:   [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
      then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A9:   not [*a,b,c,d*] in COMPLEX by A8,Th10;
      f.2 = c by A8,Lm1,Th3;
      hence thesis by A9,Def15;
    end;
  end;
  per cases;
  suppose
A10: c = 0 & d = 0;
    then [*a,b,c,d*] = [*a,b*] by Lm4;
    hence thesis by A10,Def16;
  end;
  suppose c <> 0 or d <> 0;
    then
A11: [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
    then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A12: not [*a,b,c,d*] in COMPLEX by A11,Th10;
    f.3 = d by A11,Lm1,Th3;
    hence thesis by A12,Def16;
  end;
end;

reserve z,z1,z2,z3,z4 for quaternion number;

theorem Th24:
  z = [*Rea z, Im1 z, Im2 z, Im3 z*]
proof
A1: z in QUATERNION by Def2;
  per cases;
  suppose
A2: z in COMPLEX;
    then
A3: Im2 z = 0 by Def15;
A4: Im3 z = 0 by A2,Def16;
A5: ex z9 being complex number st ( z = z9)&( Rea z = Re z9) by A2,Def13;
    consider z9 being complex number such that
A6: z = z9 and
A7: Im1 z = Im z9 by A2,Def14;
    [*Rea z, Im1 z*] = z9 by A5,A6,A7,Lm9;
    hence thesis by A3,A4,A6,Lm4;
  end;
  suppose
A8: not z in COMPLEX;
    then
A9: ex f being Function of 4,REAL st ( z = f)&( Im1 z = f.1) by Def14;
A10: ex f being Function of 4,REAL st ( z = f)&( Rea z = f.0) by A8,Def13;
A11: ex f being Function of 4,REAL st ( z = f)&( Im2 z = f.2) by A8,Def15;
A12: ex f being Function of 4,REAL st ( z = f)&( Im3 z = f.3) by A8,Def16;
    consider a,b,c,d such that
A13: z = (0,1,2,3)-->(a,b,c,d) by A9,Th22;
A14: Rea z = a by A10,A13,Lm1,Th3;
A15: Im1 z = b by A9,A13,Lm1,Th3;
A16: Im2 z = c by A11,A13,Lm1,Th3;
A17: Im3 z = d by A12,A13,Lm1,Th3;
    z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
    x.2 = 0 & x.3 = 0} by A1,A8,XBOOLE_0:def 3;
    then
A18: not z in { x where x is Element of Funcs(4,REAL):
    x.2 = 0 & x.3 = 0} by XBOOLE_0:def 5;
    reconsider f = z as Element of Funcs(4,REAL) by A13,CARD_1:52,FUNCT_2:8;
    f.2 <> 0 or f.3 <> 0 by A18;
    then c <> 0 or d <> 0 by A13,Lm1,Th3;
    hence thesis by A13,A14,A15,A16,A17,Def6;
  end;
end;

theorem Th25:
  Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 &
  Im3 z1 = Im3 z2 implies z1 = z2
proof
  assume that
A1: Rea z1 = Rea z2 and
A2: Im1 z1 = Im1 z2 and
A3: Im2 z1 = Im2 z2 and
A4: Im3 z1 = Im3 z2;
  thus z1 = [*Rea z2,Im1 z2,Im2 z2,Im3 z2*] by A1,A2,A3,A4,Th24
    .= z2 by Th24;
end;

definition
  func 0q -> quaternion number equals
  0;
  coherence by Lm7;
  func 1q -> quaternion number equals
  1;
  coherence
  proof
    [*1,0,0,0*] = [*1,0*] by Lm4;
    hence thesis by ARYTM_0:def 5;
  end;
end;

Lm10: for a, b, c, d being real number st a^2 + b^2 + c^2 + d^2 = 0 holds
a = 0 & b = 0 & c = 0 & d = 0
proof
  let a, b, c, d be real number;
  assume
A1: a^2 + b^2 + c^2 + d^2 = 0;
A2: 0 <= a^2 by XREAL_1:63;
A3: 0 <= b^2 by XREAL_1:63;
A4: 0 <= c^2 by XREAL_1:63;
A5: 0 <= d^2 by XREAL_1:63;
  assume
A6: a <> 0 or b <> 0 or c <> 0 or d <> 0;
  per cases by A6;
  suppose a <> 0;
    then 0 < a^2 + b^2 by A3,SQUARE_1:12,XREAL_1:34;
    hence contradiction by A1,A4,A5;
  end;
  suppose b <> 0;
    then 0 < a^2 + b^2 by A2,SQUARE_1:12,XREAL_1:34;
    hence contradiction by A1,A4,A5;
  end;
  suppose c <> 0;
    then 0 < c^2 + d^2 by A5,SQUARE_1:12,XREAL_1:34;
    then 0 < (a^2 + b^2) + (c^2 + d^2) by A2,A3;
    hence contradiction by A1;
  end;
  suppose d <> 0;
    then 0 < c^2 + d^2 by A4,SQUARE_1:12,XREAL_1:34;
    then 0 < (a^2 + b^2) + (c^2 + d^2) by A2,A3;
    hence contradiction by A1;
  end;
end;

theorem Th26:
  Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q
proof
  assume that
A1: Rea z = 0 and
A2: Im1 z = 0 and
A3: Im2 z = 0 and
A4: Im3 z = 0;
A5: Rea z = Rea [*0,0,0,0*] by A1,Th23;
A6: Im1 z = Im1 [*0,0,0,0*] by A2,Th23;
A7: Im2 z = Im2 [*0,0,0,0*] by A3,Th23;
  Im3 z = Im3 [*0,0,0,0*] by A4,Th23;
  hence thesis by A5,A6,A7,Lm7,Th25;
end;

theorem
  z = 0 implies (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0
proof
  assume
A1: z = 0; then
A2: Rea z = 0 by Lm7,Th23;
A3: Im1 z = 0 by A1,Lm7,Th23;
  Im2 z = 0 by A1,Lm7,Th23;
  hence thesis by A1,A2,A3,Lm7,Th23;
end;

theorem
  (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0 implies z = 0q
proof
  assume
A1: (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0;
  then
A2: Rea z = 0 by Lm10;
A3: Im1 z = 0 by A1,Lm10;
A4: Im2 z = 0 by A1,Lm10;
  Im3 z = 0 by A1,Lm10;
  hence thesis by A2,A3,A4,Th26;
end;

Lm11: [*1,0,0,0*] = 1
proof
  [*1,0,0,0*] = [*1,0*] by Lm4;
  hence thesis by ARYTM_0:def 5;
end;

theorem
  Rea (1q) = 1 & Im1(1q) = 0 & Im2 (1q) = 0 & Im3 (1q) = 0 by Lm11,Th23;

theorem Th30:
  Rea <i> = 0 & Im1 <i> = 1 & Im2 <i> = 0 & Im3 <i> = 0
proof
  [*0,1*] = [*0,1,0,0*] by Lm4;
  hence thesis by Lm3,Th23;
end;

theorem Th31:
  Rea <j> = 0 & Im1 <j> = 0 & Im2 <j> = 1 & Im3 <j> = 0 &
  Rea <k> = 0 & Im1 <k> = 0 & Im2 <k> = 0 & Im3 <k> = 1 by Th23;

Lm12: for m,n,x,y,z being quaternion number st z = m + n + x + y
holds Rea z = Rea m +Rea n +Rea x + Rea y &
Im1 z = Im1 m + Im1 n + Im1 x + Im1 y &
Im2 z = Im2 m + Im2 n + Im2 x + Im2 y & Im3 z = Im3 m + Im3 n + Im3 x + Im3 y
proof
  let m,n,x,y,z be quaternion number such that
A1: z = m + n + x + y;
  consider m1,m2,m3,m4,n1,n2,n3,n4 being Element of REAL such that
A2: m = [*m1,m2,m3,m4*] and
A3: n = [*n1,n2,n3,n4*] and
A4: m + n = [*m1+n1, m2+n2, m3+n3, m4+n4*] by Def7;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A5: x = [*x1,x2,x3,x4*] and
A6: y = [*y1,y2,y3,y4*] and
    x + y = [*x1+y1, x2+y2, x3+y3, x4+y4*] by Def7;
A7: Rea m = m1 by A2,Th23;
A8: Rea n = n1 by A3,Th23;
A9: Rea x = x1 by A5,Th23;
A10: Rea y = y1 by A6,Th23;
A11: Im1 m = m2 by A2,Th23;
A12: Im1 n = n2 by A3,Th23;
A13: Im1 x = x2 by A5,Th23;
A14: Im1 y = y2 by A6,Th23;
A15: Im2 m = m3 by A2,Th23;
A16: Im2 n = n3 by A3,Th23;
A17: Im2 x = x3 by A5,Th23;
A18: Im2 y = y3 by A6,Th23;
A19: Im3 m = m4 by A2,Th23;
A20: Im3 n = n4 by A3,Th23;
A21: Im3 x = x4 by A5,Th23;
A22: Im3 y = y4 by A6,Th23;
  m+n+x =[*m1+n1+x1, m2+n2+x2, m3+n3+x3, m4+n4+x4*] by A4,A5,Def7;
  then z = [*m1+n1+x1+y1, m2+n2+x2+y2,
  m3+n3+x3+y3, m4+n4+x4+y4*] by A1,A6,Def7;
  hence thesis by A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,A22
,Th23;
end;

Lm13: for x,y,z being quaternion number st z = x + y
holds Rea z = Rea x + Rea y & Im1 z = Im1 x + Im1 y &
Im2 z = Im2 x + Im2 y & Im3 z = Im3 x + Im3 y
proof
  let x,y,z be quaternion number such that
A1: z = x + y;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x + y = [*x1+y1, x2+y2, x3+y3, x4+y4*] by Def7;
A5: Rea x = x1 by A2,Th23;
A6: Rea y = y1 by A3,Th23;
A7: Im1 x = x2 by A2,Th23;
A8: Im1 y = y2 by A3,Th23;
A9: Im2 x = x3 by A2,Th23;
A10: Im2 y = y3 by A3,Th23;
A11: Im3 x = x4 by A2,Th23;
  Im3 y = y4 by A3,Th23;
  hence thesis by A1,A4,A5,A6,A7,A8,A9,A10,A11,Th23;
end;

Lm14: z1 + z2 = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *]
proof
  set z = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
  Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *];
  reconsider z9 = z1 + z2 as quaternion number;
A1: Rea z = Rea z1 + Rea z2 by Th23
    .= Rea z9 by Lm13;
A2: Im1 z = Im1 z1 + Im1 z2 by Th23
    .= Im1 z9 by Lm13;
A3: Im2 z = Im2 z1 + Im2 z2 by Th23
    .= Im2 z9 by Lm13;
  Im3 z = Im3 z1 + Im3 z2 by Th23
    .= Im3 z9 by Lm13;
  hence thesis by A1,A2,A3,Th25;
end;

Lm15: for x,y,z being quaternion number st z = x * y
holds Rea z = Rea x * Rea y - Im1 x * Im1 y - Im2 x * Im2 y - Im3 x * Im3 y &
Im1 z = Rea x * Im1 y + Im1 x * Rea y + Im2 x * Im3 y - Im3 x * Im2 y &
Im2 z = Rea x * Im2 y + Im2 x * Rea y + Im3 x * Im1 y - Im1 x * Im3 y &
Im3 z = Rea x * Im3 y + Im3 x * Rea y + Im1 x * Im2 y - Im2 x * Im1 y
proof
  let x,y,z be quaternion number such that
A1: z = x * y;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x * y = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
  x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *] by Def10;
A5: Rea x = x1 by A2,Th23;
A6: Rea y = y1 by A3,Th23;
A7: Im1 x = x2 by A2,Th23;
A8: Im1 y = y2 by A3,Th23;
A9: Im2 x = x3 by A2,Th23;
A10: Im2 y = y3 by A3,Th23;
A11: Im3 x = x4 by A2,Th23;
  Im3 y = y4 by A3,Th23;
  hence thesis by A1,A4,A5,A6,A7,A8,A9,A10,A11,Th23;
end;

Lm16: z1 + z2 + z3 + z4 = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 *]
proof
  set z = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
  Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
  Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 *];
  reconsider z9 = z1 + z2 + z3 + z4 as quaternion number;
A1: Rea z = Rea z1 + Rea z2 + Rea z3 + Rea z4 by Th23
    .= Rea z9 by Lm12;
A2: Im1 z = Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4 by Th23
    .= Im1 z9 by Lm12;
A3: Im2 z = Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4 by Th23
    .= Im2 z9 by Lm12;
  Im3 z = Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 by Th23
    .= Im3 z9 by Lm12;
  hence thesis by A1,A2,A3,Th25;
end;

Lm17: z1 * z2 =
[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *]
proof
  set z =
  [*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
  Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
  Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *];
  reconsider z9 = z1 * z2 as quaternion number;
A1: Rea z = Rea z1 * Rea z2 - Im1 z1 * Im1 z2 -
  Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 by Th23
    .= Rea z9 by Lm15;
A2: Im1 z = Rea z1 * Im1 z2 + Im1 z1 * Rea z2 +
  Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 by Th23
    .= Im1 z9 by Lm15;
A3: Im2 z = Rea z1 * Im2 z2 + Im2 z1 * Rea z2 +
  Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 by Th23
    .= Im2 z9 by Lm15;
  Im3 z = Rea z1 * Im3 z2 + Im3 z1 * Rea z2 +
  Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 by Th23
    .= Im3 z9 by Lm15;
  hence thesis by A1,A2,A3,Th25;
end;

Lm18: Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
  z1 * z2 =
  [*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
  Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
  Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *]
  by Lm17;
  hence thesis by Th23;
end;

theorem
  Rea (z1 + z2 + z3 + z4) = Rea z1 + Rea z2 + Rea z3 + Rea z4 &
  Im1 (z1 + z2 + z3 + z4) = Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4 &
  Im2 (z1 + z2 + z3 + z4) = Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4 &
  Im3 (z1 + z2 + z3 + z4) = Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4
proof
  (z1 + z2 + z3 + z4) = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
  Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
  Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4*] by Lm16;
  hence thesis by Th23;
end;

 reserve x for Real;

Lm19: z = x implies Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0
proof
  assume
A1: z = x;
A2: x = [*x,0*] by ARYTM_0:def 5;
  [*x,0*] = [*x,0,0,0*] by Lm4;
  hence thesis by A1,A2,Th23;
end;

theorem
  z1 = x implies Rea (z1*<i>) = 0 &
  Im1 (z1*<i>) = x & Im2 (z1*<i>) = 0 & Im3 (z1*<i>) = 0
proof
  assume
A1: z1 = x;
A2: Rea (z1 * <i>) = Rea z1 * Rea <i> - Im1 z1 * Im1 <i> - Im2 z1 * Im2 <i>
  - Im3 z1 * Im3 <i> by Lm18;
A3: Im1 (z1 * <i>) = Rea z1 * Im1 <i> + Im1 z1 * Rea <i> + Im2 z1 * Im3 <i>
  - Im3 z1 * Im2 <i> by Lm18;
A4: Im2 (z1 * <i>) = Rea z1 * Im2 <i> + Im2 z1 * Rea <i> + Im3 z1 * Im1 <i>
  - Im1 z1 * Im3 <i> by Lm18;
  Im3 (z1 * <i>) = Rea z1 * Im3 <i> + Im3 z1 * Rea <i> + Im1 z1 * Im2 <i>
  - Im2 z1 * Im1 <i> by Lm18;
  hence thesis by A1,A2,A3,A4,Lm19,Th30;
end;

theorem
  z1 = x implies Rea (z1*<j>) = 0 &
  Im1 (z1*<j>) = 0 & Im2 (z1*<j>) = x & Im3 (z1*<j>) = 0
proof
  assume
A1: z1 = x;
A2: Rea (z1 * <j>) = Rea z1 * Rea <j> - Im1 z1 * Im1 <j> - Im2 z1 * Im2 <j>
  - Im3 z1 * Im3 <j> by Lm18;
A3: Im1 (z1 * <j>) = Rea z1 * Im1 <j> + Im1 z1 * Rea <j> + Im2 z1 * Im3 <j>
  - Im3 z1 * Im2 <j> by Lm18;
A4: Im2 (z1 * <j>) = Rea z1 * Im2 <j> + Im2 z1 * Rea <j> + Im3 z1 * Im1 <j>
  - Im1 z1 * Im3 <j> by Lm18;
  Im3 (z1 * <j>) = Rea z1 * Im3 <j> + Im3 z1 * Rea <j> + Im1 z1 * Im2 <j>
  - Im2 z1 * Im1 <j> by Lm18;
  hence thesis by A1,A2,A3,A4,Lm19,Th31;
end;

theorem
  z1 = x implies Rea (z1*<k>) = 0 &
  Im1 (z1*<k>) = 0 & Im2 (z1*<k>) = 0 & Im3 (z1*<k>) = x
proof
  assume
A1: z1 = x;
A2: Rea (z1 * <k>) = Rea z1 * Rea <k> - Im1 z1 * Im1 <k> - Im2 z1 * Im2 <k>
  - Im3 z1 * Im3 <k> by Lm18;
A3: Im1 (z1 * <k>) = Rea z1 * Im1 <k> + Im1 z1 * Rea <k> + Im2 z1 * Im3 <k>
  - Im3 z1 * Im2 <k> by Lm18;
A4: Im2 (z1 * <k>) = Rea z1 * Im2 <k> + Im2 z1 * Rea <k> + Im3 z1 * Im1 <k>
  - Im1 z1 * Im3 <k> by Lm18;
  Im3 (z1 * <k>) = Rea z1 * Im3 <k> + Im3 z1 * Rea <k> + Im1 z1 * Im2 <k>
  - Im2 z1 * Im1 <k> by Lm18;
  hence thesis by A1,A2,A3,A4,Lm19,Th31;
end;

definition
  let x be Real, y be quaternion number;
  consider y1,y2,y3,y4 being Element of REAL such that
A1: y = [*y1,y2,y3,y4*] by Th7;
  func x + y means
  :Def19:
  ex y1,y2,y3,y4 being Element of REAL st y = [*y1,y2,y3,y4*] &
  it = [*x+y1,y2,y3,y4*];
  existence
  proof
    take [*x+y1,y2,y3,y4*];
    thus thesis by A1;
  end;
  uniqueness
  proof
    let c1,c2 be number;
    given y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] and
A3: c1 = [*x+y1,y2,y3,y4*];
    given y19,y29,y39,y49 being Real such that
A4: y = [*y19,y29,y39,y49*] and
A5: c2 = [*x+y19,y29,y39,y49*];
A6: y1 = y19 by A2,A4,Th12;
A7: y2 = y29 by A2,A4,Th12;
    y3 = y39 by A2,A4,Th12;
    hence thesis by A2,A3,A4,A5,A6,A7,Th12;
  end;
end;

definition
  let x be Real, y be quaternion number;
  func x - y equals
  x + -y;
  coherence;
end;

definition
  let x be Real, y be quaternion number;
  consider y1,y2,y3,y4 being Element of REAL such that
A1: y = [*y1,y2,y3,y4*] by Th7;
  func x * y means
  :Def21:
  ex y1,y2,y3,y4 being Element of REAL st y = [*y1,y2,y3,y4*] &
  it = [*x*y1,x*y2,x*y3,x*y4*];
  existence
  proof
    take [*x*y1,x*y2,x*y3,x*y4*];
    thus thesis by A1;
  end;
  uniqueness
  proof
    let c1,c2 be number;
    given y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] and
A3: c1 = [*x*y1,x*y2,x*y3,x*y4*];
    given y19,y29,y39,y49 being Real such that
A4: y = [*y19,y29,y39,y49*] and
A5: c2 = [*x*y19,x*y29,x*y39,x*y49*];
A6: y1 = y19 by A2,A4,Th12;
A7: y2 = y29 by A2,A4,Th12;
    y3 = y39 by A2,A4,Th12;
    hence thesis by A2,A3,A4,A5,A6,A7,Th12;
  end;
end;

registration
  let x be Real,z9 be quaternion number;
  cluster x+z9 -> quaternion;
  coherence
  proof
    ex y1,y2,y3,y4 being Element of REAL st z9 = [*y1,y2,y3,y4*] &
    x+z9 = [*x+y1,y2,y3,y4*] by Def19;
    hence thesis;
  end;
  cluster x*z9 -> quaternion;
  coherence
  proof
    ex y1,y2,y3,y4 being Element of REAL st z9 = [*y1,y2,y3,y4*] &
    x*z9 = [*x*y1,x*y2,x*y3,x*y4*] by Def21;
    hence x*z9 in QUATERNION;
  end;
  cluster x-z9 -> quaternion;
  coherence;
end;

Lm20: for x,y,z,w being Real holds [*x,y,z,w*] = x + y*<i> + z*<j> + w*<k>
proof
  let x,y,z,w be Real;
  <i> = [*0,1,0,0*] by Lm3,Lm4; then
A1: y*<i> = [*y*0,y*1,y*0,y*0*] by Def21
    .= [*0,y,0,0*];
A2: z*<j> = [*z*0,z*0,z*1,y*0*] by Def21
    .= [*0,0,z,0*];
A3: w*<k> = [*w*0,w*0,w*0,w*1*] by Def21
    .= [*0,0,0,w*];
  x + y* <i> = [*x+0,y,0,0*] by A1,Def19
    .= [*x,y,0,0*];
  then x + y*<i> + z*<j> = [*x+0,y+0,0+z,0+0*] by A2,Def7
    .= [*x,y,z,0*];
  then x + y*<i> + z*<j> + w*<k> = [*x+0,y+0,0+z,0+w*] by A3,Def7;
  hence thesis;
end;

definition
  let z1,z2 be quaternion number;
  redefine func z1 + z2 -> Element of QUATERNION;
  coherence by Def2;
end;

Lm21: z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)*<i> +
  (Im2 z1 + Im2 z2)*<j> + (Im3 z1 + Im3 z2)*<k>
proof
  z1 + z2 = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
  Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *] by Lm14;
  hence thesis by Lm20;
end;

theorem Th36:
  Rea (z1 + z2) = Rea z1 + Rea z2 & Im1(z1 + z2) = Im1 z1 + Im1 z2 &
  Im2 (z1 + z2) = Im2 z1 + Im2 z2 & Im3(z1 + z2) = Im3 z1 + Im3 z2
proof
  (z1 + z2) = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
  Im2 z1 + Im2 z2, Im3 z1 + Im3 z2*] by Lm14;
  hence thesis by Th23;
end;

definition
  let z1,z2 be quaternion number;
  redefine func z1 * z2 -> Element of QUATERNION;
  coherence by Def2;
end;

Lm22: z1*z2 =
 (Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
  (Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2) *<j> +
  (Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
  proof
    z1 * z2 =
    [* Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
    Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
    Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1* Im1 z2 - Im1 z1* Im3 z2,
    Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1* Im1 z2 *]
    by Lm17;
    hence thesis by Lm20;
end;

theorem
  z = Rea z+(Im1 z)*<i> + (Im2 z)*<j> + (Im3 z)*<k>
proof
  [*Rea z, Im1 z, Im2 z, Im3 z*] = z by Th24;
  hence thesis by Lm20;
end;

Lm23: for c be quaternion number holds c + 0q = c
proof
  let c be quaternion number;
A1: 0q = [*0,0*] by ARYTM_0:def 5
    .= [*0,0,0,0*] by Lm4;
  consider x,y,w,z be Element of REAL such that
A2: c = [*x,y,w,z*] by Th7;
  c + 0q = [* x+0,y+0,w+0,z+0 *] by A1,A2,Def7
    .= [*x,y,w,z*];
  hence thesis by A2;
end;

Lm24: 0*<i> = 0 & 0*<j> = 0 & 0*<k> = 0
proof
  set z1 = 0, z2 = <i>;
  consider y1,y2,y3,y4 being Element of REAL such that
A1:  <i> = [*y1,y2,y3,y4*] &
  z1*z2 = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def21;
A2: z1*z2 = [*0,0*] by A1,Lm4 .= 0 by ARYTM_0:def 5;
  consider y1,y2,y3,y4 being Element of REAL such that
A3:  <j> = [*y1,y2,y3,y4*] &
  z1*<j> = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def21;
A4: z1*<j> = [*0,0*] by A3,Lm4 .= 0 by ARYTM_0:def 5;
  consider y1,y2,y3,y4 being Element of REAL such that
A5:  <k> = [*y1,y2,y3,y4*] &
  z1*<k> = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def21;
  z1*<k> = [*0,0*] by A5,Lm4 .= 0 by ARYTM_0:def 5;
  hence thesis by A2,A4;
end;

theorem
  Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 &
  Im3 z1 = 0 & Im3 z2 = 0 implies Rea(z1*z2) = Rea z1 * Rea z2 &
  Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
  Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
  Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
  assume A1: Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 &
    Im3 z1 = 0 & Im3 z2 = 0;
A2:  z1*z2 =
  (Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
  (Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
 (Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2)*<j> +
  (Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
    by Lm22
    .= Rea z1 * Rea z2 + 0q + 0q by Lm23,Lm24,A1
    .= (Rea z1 * Rea z2) + 0q by Lm23;
    consider y1,y2,y3,y4 being Element of REAL such that
A3: 0q = [*y1,y2,y3,y4*] &
    (Rea z1 * Rea z2) + 0q = [*(Rea z1 * Rea z2)+y1,y2,y3,y4*] by Def19;
    y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by Th12,A3,Lm7; then
    (Rea z1 * Rea z2) + 0q = [*(Rea z1 * Rea z2),0*] by A3,Lm4; then
    (Rea z1 * Rea z2) + 0q = Rea z1 * Rea z2 by ARYTM_0:def 5;
    hence thesis by Lm19,A2,A1;
end;

theorem
  Rea z1 = 0 & Rea z2 = 0 implies
  Rea(z1*z2) = - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
  Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
  Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
  Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
  assume A1: Rea z1 = 0 & Rea z2 = 0;
    Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
  by Lm18;
    hence thesis by A1;
end;

theorem
  Rea(z*z) = (Rea z)^2 - (Im1 z)^2 - (Im2 z)^2 - (Im3 z)^2 &
  Im1(z*z) = 2*(Rea z * Im1 z) & Im2(z*z) = 2*( Rea z * Im2 z) &
  Im3(z*z) = 2*(Rea z * Im3 z)
proof
  Rea (z * z) =
    Rea z * Rea z - Im1 z * Im1 z - Im2 z * Im2 z - Im3 z * Im3 z &
  Im1 (z * z) =
    Rea z * Im1 z + Im1 z * Rea z + Im2 z * Im3 z - Im3 z * Im2 z &
  Im2 (z * z) =
    Rea z * Im2 z + Im2 z * Rea z + Im3 z * Im1 z - Im1 z * Im3 z &
  Im3 (z * z) =
    Rea z * Im3 z + Im3 z * Rea z + Im1 z * Im2 z - Im2 z * Im1 z by Lm18;
  hence thesis;
end;

definition
  let z be quaternion number;
  redefine func -z -> Element of QUATERNION;
  coherence by Def2;
end;

Lm25: -z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k>
  proof
    set z9 = [* -Rea z, -Im1 z, -Im2 z, -Im3 z *];
A1: z9 = -Rea z+(-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm20;
    z9 + z =
    [* Rea z9 + Rea z, Im1 z9 + Im1 z, Im2 z9 + Im2 z,Im3 z9 + Im3 z*] by Lm14
      .= [* -Rea z + Rea z, Im1 z9 + Im1 z,Im2 z9 + Im2 z,Im3 z9 + Im3 z *]
    by Th23
      .= [* 0, - Im1 z + Im1 z,Im2 z9 + Im2 z,Im3 z9 + Im3 z *] by Th23
      .= [* 0, 0,- Im2 z + Im2 z,Im3 z9 + Im3 z *] by Th23
      .= [* 0, 0,0,-Im3 z + Im3 z *] by Th23
      .= 0 by Lm7;
    hence thesis by A1,Def8;
end;

theorem Th41:
  Rea(-z) = -(Rea z) & Im1(-z) = -(Im1 z) & Im2(-z) = -(Im2 z) &
  Im3(-z) = -(Im3 z)
proof
  -z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm25; then
  -z = [*-Rea z,-Im1 z,-Im2 z,-Im3 z*] by Lm20;
  hence thesis by Th23;
end;

definition
  let z1,z2 be quaternion number;
  redefine func z1 - z2 -> Element of QUATERNION;
  coherence by Def2;
end;

Lm26: z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
  (Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k>
proof
    z1 - z2 = Rea z1 + Rea (-z2) + (Im1 z1 + Im1 (-z2))*<i> +
    (Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Lm21
      .= Rea z1 + -Rea z2 + (Im1 z1 + Im1 (-z2))*<i> +
    (Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th41
      .= Rea z1 + -Rea z2 + (Im1 z1 - Im1 z2)*<i> +
    (Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th41
      .= Rea z1 + -Rea z2 + (Im1 z1 - Im1 z2)*<i> +
    (Im2 z1 + -Im2 z2)*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th41
      .= (Rea z1 - Rea z2) + (Im1 z1 - Im1 z2)*<i> +
    (Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Th41;
    hence thesis;
end;

theorem Th42:
  Rea(z1 - z2) = Rea z1 - Rea z2 & Im1(z1 - z2) = Im1 z1 - Im1 z2 &
  Im2(z1 - z2) = Im2 z1 - Im2 z2 & Im3(z1 - z2) = Im3 z1 - Im3 z2
proof
  z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
    (Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Lm26; then
  z1 - z2 = [*Rea z1 - Rea z2, Im1 z1 - Im1 z2,
    Im2 z1 - Im2 z2, Im3 z1 - Im3 z2*] by Lm20;
  hence thesis by Th23;
end;

definition
  let z be quaternion number;
  func z*' -> quaternion number equals
  Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k>;
  coherence;
end;

definition
  let z be quaternion number;
  redefine func z*' -> Element of QUATERNION;
  coherence;
end;

theorem Th43:
  z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*]
proof
  <i> = [*0,1,0,0*] by Lm3,Lm4;
  then z*'= Rea z + [*(-Im1 z)*0,(-Im1 z) *1,(-Im1 z) *0,(-Im1 z) *0 *]
  + (-Im2 z)*<j> + (-Im3 z)*<k> by Def21
    .= Rea z + [*0,-Im1 z,0,0 *] +
  [*(-Im2 z)*0,(-Im2 z)*0,(-Im2 z)*1,(-Im2 z)*0*] + (-Im3 z)*<k> by Def21
    .= Rea z + [*0,-Im1 z,0,0 *] + [*0,0,(-Im2 z),0*] +
  [*(-Im3 z)*0,(-Im3 z)*0,(-Im3 z)*0,(-Im3 z)*1*] by Def21
    .= [*Rea z+0,-Im1 z,0,0 *] + [*0,0,(-Im2 z),0*]
  + [*0,0,0,(-Im3 z)*] by Def19
    .= [*Rea z+0,-Im1 z+0,0+(-Im2 z),0+0*] + [*0,0,0,(-Im3 z)*] by Def7
    .= [*Rea z+0,-Im1 z+0,-Im2 z+0,0+(-Im3 z)*] by Def7;
  hence thesis;
end;

theorem
  Rea (z*') = Rea z & Im1 (z*') = -Im1 z &
  Im2 (z*') = -Im2 z & Im3 (z*') = -Im3 z
proof
  z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Lm20;
  hence thesis by Th23;
end;

theorem
  z = 0 implies z*' = 0
proof
  assume
A1: z = 0; then
A2: Rea z = 0 by Lm7,Th23;
A3: Im1 z = 0 by A1,Lm7,Th23;
A4: Im2 z = 0 by A1,Lm7,Th23;
  Im3 z = 0 by A1,Lm7,Th23;
  hence thesis by A2,A3,A4,Lm7,Th43;
end;

theorem
  z*' = 0 implies z = 0
proof
  assume
A1: z*' = 0;
A2: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43;
A3: Rea z*' = 0 by A1,Lm7,Th23;
A4: Im1 z*' = 0 by A1,Lm7,Th23;
A5: Im2 z*'= 0 by A1,Lm7,Th23;
A6: Im3 z*' = 0 by A1,Lm7,Th23;
A7: Rea z*' = Rea z by A2,Th23;
A8: Im1 z*' = -Im1 z by A2,Th23;
A9: Im2 z*'= -Im2 z by A2,Th23;
  Im3 z*' = -Im3 z by A2,Th23;
  hence thesis by A3,A4,A5,A6,A7,A8,A9,Th26;
end;

theorem
  1q*' = 1q
proof
  [*1,0*] = [*1,0,0,0*] by Lm4; then
A1: 1q = [*1,0,0,0*] by ARYTM_0:def 5;
A2: Rea [*1,0,0,0*] = 1 by Th23;
A3: Im1 [*1,0,0,0*] = 0 by Th23;
A4: Im2 [*1,0,0,0*] = 0 by Th23;
  Im3 [*1,0,0,0*] = 0 by Th23;
  hence thesis by A1,A2,A3,A4,Th43;
end;

theorem
  Rea (<i>*') = 0 & Im1 (<i>*') = -1 & Im2 (<i>*') = 0 & Im3 (<i>*') = 0
proof
  <i>*' = [*0, -1, 0, 0*] by Th30,Th43;
  hence thesis by Th23;
end;

theorem
  Rea (<j>*') = 0 & Im1 (<j>*') = 0 & Im2 (<j>*') = -1 & Im3 (<j>*') = 0
proof
  <j>*' = [*0,0,-1,0*] by Th31,Th43;
  hence thesis by Th23;
end;

theorem
  Rea (<k>*') = 0 & Im1 (<k>*') = 0 & Im2 (<k>*') = 0 & Im3 (<k>*') = -1
proof
  <k>*' = [*0,0,0,-1*] by Th31,Th43;
  hence thesis by Th23;
end;

theorem
  <i>*' = -<i> by Th30,Lm25;

theorem
  <j>*' = -<j> by Th31,Lm25;

theorem
  <k>*' = -<k> by Th31,Lm25;

theorem
  (z1 + z2)*' = z1*' + z2*'
proof
A1: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th43;
A2: z2*' = [*Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th43;
A3: (z1+z2)*' = [*Rea (z1+z2), -Im1 (z1+z2), -Im2 (z1+z2), -Im3 (z1+z2)*]
  by Th43;
  z1*' + z2*' = [* Rea z1 + Rea z2, - Im1 z1 + - Im1 z2,
  - Im2 z1 + - Im2 z2, - Im3 z1 + - Im3 z2*] by A1,A2,Def7
    .= [* Rea (z1 + z2), - (Im1 z1 + Im1 z2),
  - (Im2 z1 + Im2 z2), - (Im3 z1 + Im3 z2)*] by Th36
    .= [* Rea (z1 + z2), - Im1 (z1 + z2),
  - (Im2 z1 + Im2 z2), - (Im3 z1 + Im3 z2)*] by Th36
    .= [* Rea (z1 + z2), - Im1 (z1 + z2),
  - Im2 (z1+z2), - (Im3 z1 + Im3 z2)*] by Th36;
  hence thesis by A3,Th36;
end;

theorem Th55:
  (-z)*' = -(z*')
proof
A1: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43;
  (-z)*' = [*Rea (-z), -Im1 (-z), -Im2 (-z), -Im3 (-z)*] by Th43;
  then (-z)*' = [*-Rea z, -Im1 (-z), -Im2 (-z), -Im3 (-z)*] by Th41
    .= [*-Rea z, - - Im1 z, -Im2 (-z), -Im3 (-z)*] by Th41
    .= [*-Rea z, Im1 z, - - Im2 z, -Im3 (-z)*] by Th41
    .= [*-Rea z, Im1 z, Im2 z, - -Im3 z*] by Th41
    .= [*-Rea z, Im1 z, Im2 z, Im3 z*];
  then z*' + (-z)*' = [*Rea z+ -Rea z, -Im1 z+ Im1 z,
  -Im2 z+ Im2 z, -Im3 z+Im3 z*] by A1,Def7 .= 0 by Lm7;
  hence thesis by Def8;
end;

theorem
  (z1 - z2)*' = z1*' - z2*'
proof
A1: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th43;
A2: (-z2)*' = [*Rea (-z2), -Im1 (-z2), -Im2 (-z2), -Im3 (-z2)*] by Th43;
A3: (z1-z2)*' = [*Rea (z1-z2), -Im1 (z1-z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
  by Th43;
A4: z1*' - z2*' = z1*' + (- z2)*' by Th55
    .= [*Rea z1+Rea (-z2), -Im1 z1+ -Im1(-z2),
  -Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by A1,A2,Def7
    .= [*Rea z1+- Rea z2, -Im1 z1+ -Im1(-z2),
  -Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by Th41
    .= [*Rea z1- Rea z2, -Im1 z1- - Im1 z2,
  -Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by Th41
    .= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2,
  -Im2 z1 - - Im2 z2, -Im3 z1+ - Im3 (-z2)*] by Th41
    .= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2,
  -Im2 z1 + Im2 z2, -Im3 z1 - -Im3 z2*] by Th41
    .= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2, -Im2 z1 + Im2 z2, -Im3 z1 +Im3 z2*];
  (z1-z2)*' = [*Rea z1-Rea z2, -Im1 (z1-z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
  by A3,Th42
    .= [*Rea z1-Rea z2, -(Im1 z1- Im1 z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
  by Th42
    .= [*Rea z1-Rea z2, -Im1 z1+ Im1 z2,
  -(Im2 z1- Im2 z2), -Im3 (z1-z2)*] by Th42
    .= [*Rea z1-Rea z2, -Im1 z1+ Im1 z2,
  -Im2 z1+ Im2 z2, -(Im3 z1- Im3 z2)*] by Th42;
  hence thesis by A4;
end;

theorem
  (z1*z2)*' = z1*' * z2*' implies (Im2 z1 * Im3 z2) = (Im3 z1)*(Im2 z2)
proof
  assume
A1: (z1*z2)*' = z1*' * z2*';
A2: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th43;
A3: z2*' = [*Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th43;
A4: (z1*z2)*' = [*Rea (z1*z2), -Im1 (z1*z2), -Im2 (z1*z2), -Im3 (z1*z2)*]
  by Th43;
A5: z1*' * z2*' = [*(Rea z1)*(Rea z2) - (- Im1 z1)*(- Im1 z2) -
  (- Im2 z1)*(- Im2 z2) - (-Im3 z1)*(-Im3 z2),
  (Rea z1)*(- Im1 z2) + (- Im1 z1)*(Rea z2) +
  (- Im2 z1)*(-Im3 z2) - (-Im3 z1)*(- Im2 z2),
  (Rea z1)*(- Im2 z2) + (Rea z2)*(- Im2 z1) +
  (- Im1 z2)*(-Im3 z1) - (-Im3 z2)*(- Im1 z1),
  (Rea z1)*(-Im3 z2) + (-Im3 z1)*(Rea z2) +
  (- Im1 z1)*(- Im2 z2) - (- Im2 z1)*(- Im1 z2) *] by A2,A3,Def10
    .= [*(Rea z1)*(Rea z2) - (Im1 z1)*(Im1 z2) -
  (Im2 z1)*(Im2 z2) - (Im3 z1)*(Im3 z2),
  -(Rea z1)*( Im1 z2) - ( Im1 z1)*(Rea z2) +
  (Im2 z1)*(Im3 z2) - (Im3 z1)*(Im2 z2),
  -(Rea z1)*(Im2 z2) - (Rea z2)*(Im2 z1) +
  (Im1 z2)*(Im3 z1) - (Im3 z2)*(Im1 z1),
  -(Rea z1)*(Im3 z2) - (Im3 z1)*(Rea z2) +
  (Im1 z1)*(Im2 z2) - (Im2 z1)*(Im1 z2) *];
A6: (z1*z2)*' =
  [*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  -Im1 (z1*z2), -Im2 (z1*z2), -Im3 (z1*z2)*] by A4,Lm18
    .=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  -(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
  -Im2 (z1*z2), -Im3 (z1*z2)*] by Lm18
    .=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  -(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
  -(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2),
  -Im3 (z1*z2)*] by Lm18
    .=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
  -(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
  -(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2),
  -(Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*]
  by Lm18
    .=[*Rea z1 * Rea z2 - (Im1 z1 * Im1 z2) -
  (Im2 z1 * Im2 z2) - (Im3 z1 * Im3 z2),
  -(Rea z1 * Im1 z2) - (Im1 z1 * Rea z2) -
  (Im2 z1 * Im3 z2) + (Im3 z1 * Im2 z2),
  -(Rea z1 * Im2 z2) - (Im2 z1 * Rea z2) -
  (Im3 z1 * Im1 z2) + (Im1 z1 * Im3 z2),
  -(Rea z1 * Im3 z2) - (Im3 z1 * Rea z2) -
  (Im1 z1 * Im2 z2) + (Im2 z1 * Im1 z2)*];
A7: Im1 (z1*' * z2*') = -(Rea z1)*( Im1 z2) - ( Im1 z1)*(Rea z2) +
  (Im2 z1)*(Im3 z2) - (Im3 z1)*(Im2 z2) by A5,Th23;
  Im1(z1*z2)*' = -(Rea z1 * Im1 z2) - (Im1 z1 * Rea z2) -
  (Im2 z1 * Im3 z2) + (Im3 z1 * Im2 z2) by A6,Th23;
  hence thesis by A1,A7;
end;

theorem
  Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z*' = z
proof
  assume that
A1: Im1 z = 0 and
A2: Im2 z = 0 and
A3: Im3 z = 0;
A4: z = [*Rea z,0,0,0*] by A1,A2,A3,Th24
    .= [*Rea z,0*] by Lm4
    .= Rea z by ARYTM_0:def 5;
  z*' = [*Rea z, 0,0,0*] by A1,A2,A3,Th43
    .= [*Rea z, 0*] by Lm4
    .= Rea z by ARYTM_0:def 5;
  hence thesis by A4;
end;

theorem
  Rea z = 0 implies z*' = -z
proof
  assume A1: Rea z = 0;
  -z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm25;
  hence thesis by A1;
end;

theorem
  Rea(z*z*') = (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2 &
  Im1(z*z*') = 0 & Im2(z*z*') = 0 & Im3(z*z*') = 0
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th24;
  z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43;
  then z*z*' = [* Rea z*Rea z-(Im1 z)*(-Im1 z)-Im2 z*(-Im2 z)-(Im3 z)*(-Im3
  z), Rea z*(-Im1 z)+Im1 z*Rea z+Im2 z*(-Im3 z)-(Im3 z)*(-Im2 z),
  Rea z*(-Im2 z)+Rea z*Im2 z+(-Im1 z)*(Im3 z)-(-Im3 z)*Im1 z,
  Rea z*(-Im3 z)+(Im3 z)*Rea z+Im1 z*(-Im2 z)-Im2 z*(-Im1 z) *] by A1,Def10
    .= [* (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2,0,0,0 *];
  hence thesis by Th23;
end;

theorem
  Rea(z + z*') = 2*Rea z & Im1(z + z*') = 0 &
  Im2(z + z*') = 0 & Im3(z + z*') = 0
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th24;
  z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43;
  then z + z*' = [*Rea z+Rea z, Im1 z+ -Im1 z, Im2 z+ -Im2 z, Im3 z+ -Im3 z*]
  by A1,Def7
    .=[*2*Rea z,0,0,0*];
  hence thesis by Th23;
end;

theorem Th62:
  -z = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*]
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th24;
  set z9 = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*];
  z + z9 = [*Rea z+ -Rea z, Im1 z+ -Im1 z, Im2 z+ -Im2 z, Im3 z+ -Im3 z*]
  by A1,Def7
    .= 0 by Lm7;
  hence thesis by Def8;
end;

theorem
  z1 - z2 =
    [*Rea z1 - Rea z2, Im1 z1 - Im1 z2, Im2 z1 - Im2 z2, Im3 z1 - Im3 z2*]
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th24;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th24;
  set z9 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*];
  z2 + z9 = [*Rea z2+ -Rea z2, Im1 z2+ -Im1 z2,
  Im2 z2+ -Im2 z2, Im3 z2+ -Im3 z2*] by A2,Def7
    .= 0 by Lm7;
  then -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Def8;
  hence thesis by A1,Def7;
end;

theorem
  Rea(z - z*') = 0 & Im1(z - z*') = 2*Im1 z &
  Im2(z - z*') = 2*Im2 z & Im3(z - z*') = 2*Im3 z
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th24;
A2: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43;
A3: Im1 z*' = - Im1 z by A2,Th23;
A4: Im2 z*' = - Im2 z by A2,Th23;
A5: Im3 z*' = - Im3 z by A2,Th23;
  set zz = z*';
  -zz = [*-Rea zz, -Im1 zz, -Im2 zz, -Im3 zz*] by Th62;
  then -zz = [*-Rea z,Im1 z,Im2 z,Im3 z*] by A2,Th23,A3,A4,A5;
  then z - zz = [*Rea z+ (-Rea z), Im1 z + Im1 z, Im2 z + Im2 z, Im3 z +Im3
  z *] by A1,Def7
    .= [*0, 2* Im1 z, 2* Im2 z,2* Im3 z*];
  hence thesis by Th23;
end;

definition let z;
  func |.z.| -> real number equals
  sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2);
  coherence;
end;

theorem Th65:
  |.0q.| = 0
proof
A1: Rea 0q = 0 by Lm7,Th23;
A2: Im1 0q = 0 by Lm7,Th23;
  Im2 0q = 0 by Lm7,Th23;
  hence thesis by A1,A2,Lm7,Th23,SQUARE_1:17;
end;

theorem Th66:
  |.z.| = 0 implies z = 0
proof
  assume
A1: |.z.| = 0;
A2: 0 <= (Rea z)^2 by XREAL_1:63;
A3: 0 <= (Im1 z)^2 by XREAL_1:63;
A4: 0 <= (Im2 z)^2 by XREAL_1:63;
  0 <= (Im3 z)^2 by XREAL_1:63; then
A5: 0 = (Rea z)^2+(Im1 z)^2+ (Im2 z)^2 + (Im3 z)^2
    by A1,A2,A3,A4,SQUARE_1:25; then
A6: Rea z = 0 by Lm10;
A7: Im1 z = 0 by A5,Lm10;
A8: Im2 z = 0 by A5,Lm10;
  Im3 z = 0 by A5,Lm10;
  hence thesis by A6,A7,A8,Lm7,Th24;
end;

theorem Th67:
  0 <= |.z.|
proof
A1: 0 <= (Rea z)^2 by XREAL_1:63;
A2: 0 <= (Im1 z)^2 by XREAL_1:63;
A3: 0 <= (Im2 z)^2 by XREAL_1:63;
  0 <= (Im3 z)^2 by XREAL_1:63;
  hence thesis by A1,A2,A3,SQUARE_1:def 2;
end;

theorem
  |.1q.| = 1
proof
A1: Rea 1q =1 by Lm11,Th23;
A2: Im1 1q = 0 by Lm11,Th23;
  Im2 1q = 0 by Lm11,Th23;
  hence thesis by A1,A2,Lm11,Th23,SQUARE_1:18;
end;

theorem
  |.<i>.| = 1 by Th30,SQUARE_1:18;

theorem
  |.<j>.| = 1 by Th31,SQUARE_1:18;

theorem
  |.<k>.| = 1 by Th31,SQUARE_1:18;

theorem Th72:
  |.-z.| = |.z.|
proof
A1: -z = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th62;
  then
A2: Rea -z = - Rea z by Th23;
A3: Im1 -z = - Im1 z by A1,Th23;
A4: Im2 -z = - Im2 z by A1,Th23;
  Im3 -z = - Im3 z by A1,Th23;
  hence thesis by A2,A3,A4;
end;

theorem Th73:
  |.z*'.| = |.z.|
proof
A1: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th43; then
A2: Im1 z*' = - Im1 z by Th23;
A3: Im2 z*' = - Im2 z by A1,Th23;
  Im3 z*' = - Im3 z by A1,Th23;
  hence thesis by A1,A2,A3,Th23;
end;

theorem Th74:
  for a,b,c,d being real number holds a^2 + b^2 + c^2 + d^2 >= 0
proof
  let a,b,c,d be real number;
A1: a^2 >= 0 by XREAL_1:63;
A2: b^2>= 0 by XREAL_1:63;
A3: c^2 >= 0 by XREAL_1:63;
  d^2 >= 0 by XREAL_1:63;
  hence thesis by A1,A2,A3;
end;

Lm27: a^2 <= a^2 + b^2 + c^2 + d^2
proof
A1: 0 <= c^2 by XREAL_1:63;
A2: 0<= d^2 by XREAL_1:63;
  a^2 <= a^2 + b^2 by XREAL_1:31,63;
  then 0+a^2 <= (a^2 + b^2) + c^2 by A1,XREAL_1:7;
  hence thesis by A2,XREAL_1:7;
end;

Lm28: for a, b, c, d being real number holds c^2 <= a^2 + b^2 + c^2 + d^2
proof
  let a, b, c, d be real number;
A1: 0 <= b^2 by XREAL_1:63;
A2: 0 <= d^2 by XREAL_1:63;
  c^2 <= a^2 + c^2 by XREAL_1:31,63;
  then 0+c^2 <= (a^2 + c^2) + b^2 by A1,XREAL_1:7;
  hence thesis by A2,XREAL_1:7;
end;

Lm29: d^2 <= a^2 + b^2 + c^2 + d^2
proof
A1: 0 <= b^2 by XREAL_1:63;
A2: 0 <= c^2 by XREAL_1:63;
  d^2 <= a^2 + d^2 by XREAL_1:31,63;
  then 0+d^2 <= (a^2 + d^2) + c^2 by A2,XREAL_1:7;
  then 0+ d^2 <= b^2 + (a^2 + d^2 + c^2) by A1,XREAL_1:7;
  hence thesis;
end;

Lm30: a >= b^2 implies sqrt a >= b
proof
  assume
A1: a >= b^2;
  b^2 >= 0 by XREAL_1:63; then
A2: sqrt a >= sqrt b^2 by A1,SQUARE_1:26;
  per cases;
  suppose b >= 0;
    hence thesis by A2,SQUARE_1:22;
  end;
  suppose
A3: b < 0;
    then sqrt a >= -b by A2,SQUARE_1:23;
    hence thesis by A3;
  end;
end;

Lm31: for a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 being real number st
a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds
a1 + a2 + a3 + a4 + a5 + a6 >= b1 + b2 + b3 + b4 + b5 + b6
proof
  let a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 be real number;
  assume that
A1: a1 >= b1 and
A2: a2 >= b2 and
A3: a3 >= b3 and
A4: a4 >= b4 and
A5: a5 >= b5 and
A6: a6 >= b6;
A7: a1+a2>=b1+b2 by A1,A2,XREAL_1:7;
A8: a3+a4 >= b3+b4 by A3,A4,XREAL_1:7;
A9: a5+a6 >= b5+b6 by A5,A6,XREAL_1:7;
  (a1+a2)+(a3+a4)>=(b1+b2) + (b3+b4) by A7,A8,XREAL_1:7;
  then (a1+a2)+(a3+a4)+(a5+a6)>=(b1+b2) + (b3+b4)+(b5+b6) by A9,XREAL_1:7;
  hence thesis;
end;

Lm32: a>=0 & b>=0 & a^2 >= b^2 implies a >= b
proof
  assume that
A1: a>=0 and
A2: b>=0 and
A3: a^2 >= b^2;
  sqrt a^2 >= sqrt b^2 by A2,A3,SQUARE_1:26;
  then a >= sqrt b^2 by A1,SQUARE_1:22;
  hence thesis by A1,SQUARE_1:22;
end;

Lm33: for m1,m2,m4,m3,n1,n2,n3,n4 being real number holds
(sqrt (m1^2 + m2^2 + m3^2 + m4^2)+sqrt (n1^2 + n2^2 + n3^2 + n4^2))^2
= (m1^2 + m2^2 + m3^2 + m4^2 + n1^2 + n2^2 + n3^2 + n4^2)+
2*sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2))
proof
  let m1,m2,m4,m3,n1,n2,n3,n4 be real number;
  set a = m1^2 + m2^2 + m3^2 + m4^2, b = n1^2 + n2^2 + n3^2 + n4^2;
A1: a >= 0 by Th74;
A2: b>= 0 by Th74;
  (sqrt a + sqrt b)^2 = (sqrt a)^2 + 2*(sqrt a)*(sqrt b) + (sqrt b)^2
    .= a + 2*(sqrt a)*(sqrt b) + (sqrt b)^2 by A1,SQUARE_1:def 2
    .= a + 2*((sqrt a)*(sqrt b)) + b by A2,SQUARE_1:def 2
    .= a + 2*sqrt (a* b) + b by A1,A2,SQUARE_1:29;
  hence thesis;
end;

Lm34: for m1,m2,m3,m4,n1,n2,n3,n4 being real number holds
(sqrt ((m1 + n1)^2 + (m2+n2)^2 + (m3+n3)^2 + (m4 +n4)^2))^2
= (m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2
proof
  let m1,m2,m3,m4,n1,n2,n3,n4 be real number;
  (m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2 >= 0 by Th74;
  hence thesis by SQUARE_1:def 2;
end;

theorem
  Rea z <= |.z.|
proof
  0 <= (Rea z)^2 by XREAL_1:63; then
  A1: sqrt ((Rea z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
  by Lm27,SQUARE_1:26;
  per cases;
  suppose Rea z >= 0;
    hence thesis by A1,SQUARE_1:22;
  end;
  suppose
A2: Rea z < 0;
    then - Rea z <= |.z.| by A1,SQUARE_1:23;
    hence thesis by A2;
  end;
end;

theorem
  Im1 z <= |.z.|
proof
  0 <= (Im1 z)^2 by XREAL_1:63;
  then
  A1: sqrt ((Im1 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
  by Lm27,SQUARE_1:26;
  per cases;
  suppose Im1 z >= 0;
    hence thesis by A1,SQUARE_1:22;
  end;
  suppose
A2: Im1 z < 0;
    then -Im1 z <= |.z.| by A1,SQUARE_1:23;
    hence thesis by A2;
  end;
end;

theorem
  Im2 z <= |.z.|
proof
  0 <= (Im2 z)^2 by XREAL_1:63;
  then
  A1: sqrt ((Im2 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
  by Lm28,SQUARE_1:26;
  per cases;
  suppose Im2 z >= 0;
    hence thesis by A1,SQUARE_1:22;
  end;
  suppose
A2: Im2 z < 0;
    then -Im2 z <= |.z.| by A1,SQUARE_1:23;
    hence thesis by A2;
  end;
end;

theorem
  Im3 z <= |.z.|
proof
  0<= (Im3 z)^2 by XREAL_1:63; then
  A1: sqrt ((Im3 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
  by Lm29,SQUARE_1:26;
  per cases;
  suppose Im3 z >= 0;
    hence thesis by A1,SQUARE_1:22;
  end;
  suppose
A2: Im3 z < 0;
    then -Im3 z <= |.z.| by A1,SQUARE_1:23;
    hence thesis by A2;
  end;
end;

theorem Th79:
  |.z1 + z2.| <= |.z1.| + |.z2.|
proof
  set m1 = Rea z1, m2 = Im1 z1, m3 = Im2 z1, m4 = Im3 z1,
  n1 = Rea z2, n2 = Im1 z2, n3 = Im2 z2, n4 = Im3 z2, a = m1^2+m2^2+m3^2+m4^2,
  b = n1^2 +n2^2 + n3^2 + n4^2;
A1: |.z1.| >= 0 by Th67;
  |.z2.| >= 0 by Th67; then
A2: |.z1.| + |.z2.| >= 0 by A1;
A3: (sqrt (m1^2 + m2^2 + m3^2 + m4^2)+sqrt (n1^2 + n2^2 + n3^2 + n4^2))^2
  = (m1^2 + m2^2 + m3^2 + m4^2 + n1^2 + n2^2 + n3^2 + n4^2)+
  2*sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2)) by Lm33;
A4: (sqrt ((m1 + n1)^2 + ( m2+n2)^2 + (m3+n3)^2 + (m4 +n4)^2))^2
  = (m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2 by Lm34;
A5: Rea (z1+z2) = Rea z1 + Rea z2 by Th36;
A6: Im1 (z1+z2) = Im1 z1 + Im1 z2 by Th36;
A7: Im2 (z1+z2) = Im2 z1 + Im2 z2 by Th36;
A8: Im3 (z1+z2) = Im3 z1 + Im3 z2 by Th36;
A9: (m1*n2)^2 + (m2*n1)^2 >= 2*(m1*n2)*(m2*n1) by SERIES_3:6;
A10: (m1*n3)^2 + (m3*n1)^2 >= 2*(m1*n3)*(m3*n1) by SERIES_3:6;
A11: (m1*n4)^2 + (m4*n1)^2 >= 2*(m1*n4)*(m4*n1) by SERIES_3:6;
A12: (m2*n3)^2 + (m3*n2)^2 >= 2*(m2*n3)*(m3*n2) by SERIES_3:6;
A13: (m2*n4)^2 + (m4*n2)^2 >= 2*(m2*n4)*(m4*n2) by SERIES_3:6;
A14: (m3*n4)^2 + (m4*n3)^2 >= 2*(m3*n4)*(m4*n3) by SERIES_3:6;
  set a1= (m1*n2)^2, a2= (m2*n1)^2, a3=(m1*n3)^2,a4= (m3*n1)^2,
  a5= (m1*n4)^2, a6= (m4*n1)^2, a7= (m2*n3)^2, a8= (m3*n2)^2,
  a9 =(m2*n4)^2, a10= (m4*n2)^2, a11= (m3*n4)^2,a12= (m4*n3)^2,
  b1= 2*(m1*n2)*(m2*n1), b2= 2*(m1*n3)*(m3*n1),
  b3 = 2*(m1*n4)*(m4*n1), b4= 2*(m2*n3)*(m3*n2),
  b5= 2*(m2*n4)*(m4*n2), b6 =2*(m3*n4)*(m4*n3);
  ((a1 + a2) + (a3 + a4) + (a5 + a6)+(a7 + a8) + (a9 + a10) + (a11 + a12)) >=
  b1 + b2 + b3 + b4 + b5 + b6 by A9,A10,A11,A12,A13,A14,Lm31;
  then (a1 + a2 + a3 + a4 + a5 + a6+a7 + a8 + a9 + a10 + a11 + a12)
  +((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) >= (b1 + b2 + b3 + b4 + b5 + b6)
  +((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) by XREAL_1:6;
  then (a1 + a2 + a3 + a4 + a5 + a6+a7 + a8 + a9 + a10 + a11 + a12 )
  +((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) >= (m1*n1+m2*n2+m3*n3+m4*n4)^2;
  then sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
  m1*n1+m2*n2+m3*n3+m4*n4 by Lm30;
  then 2*sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
  2*(m1*n1+m2*n2+m3*n3+m4*n4) by XREAL_1:64;
  then (a+b)+2*sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
  (a+b)+2*(m1*n1+m2*n2+m3*n3+m4*n4) by XREAL_1:6;
  hence thesis by A2,A3,A4,A5,A6,A7,A8,Lm32;
end;

theorem Th80:
  |.z1 - z2.| <= |.z1.| + |.z2.|
proof
  |.z1 - z2.| <= |.z1.| + |.-z2.| by Th79;
  hence thesis by Th72;
end;

Lm35: z1 = z1+z2-z2
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th24;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th24;
A3: -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th62;
  z1 + z2 = [*Rea z1+ Rea z2, Im1 z1+ Im1 z2,
  Im2 z1+ Im2 z2, Im3 z1+ Im3 z2*] by A1,A2,Def7;
  then z1+z2-z2 = [*Rea z1+ Rea z2 -Rea z2, Im1 z1+ Im1 z2-Im1 z2,
  Im2 z1+ Im2 z2-Im2 z2, Im3 z1+ Im3 z2-Im3 z2*] by A3,Def7;
  hence thesis by Th24;
end;

Lm36: z1 = z1-z2+z2
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th24;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th24;
  -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th62;
  then z1 - z2 = [*Rea z1+ -Rea z2, Im1 z1+ -Im1 z2,
  Im2 z1+ -Im2 z2, Im3 z1+ -Im3 z2*] by A1,Def7;
  then z1-z2+z2 = [*Rea z1+ -Rea z2 +Rea z2, Im1 z1+ -Im1 z2+ Im1 z2,
  Im2 z1+ -Im2 z2+ Im2 z2, Im3 z1+ -Im3 z2+ Im3 z2*] by A2,Def7
    .= [*Rea z1+ Rea z2 -Rea z2, Im1 z1+ Im1 z2-Im1 z2,
  Im2 z1+ Im2 z2-Im2 z2, Im3 z1+ Im3 z2-Im3 z2*];
  hence thesis by Th24;
end;

Lm37: z1-z2 = [*Rea z1-Rea z2, Im1 z1-Im1 z2, Im2 z1-Im2 z2, Im3 z1-Im3 z2*]
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th24;
  -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th62;
  hence thesis by A1,Def7;
end;

Lm38: z1-z2 = -(z2 - z1)
proof
A1: Rea (z2 - z1) = Rea z2 - Rea z1 by Th42;
A2: Im1 (z2 - z1) = Im1 z2 - Im1 z1 by Th42;
A3: Im2 (z2 - z1) = Im2 z2 - Im2 z1 by Th42;
A4: Im3 (z2 - z1) = Im3 z2 - Im3 z1 by Th42;
A5: Rea (-(z2 - z1)) = -(Rea z2 - Rea z1) by A1,Th41;
A6: Im1 (-(z2 - z1)) = -(Im1 z2 - Im1 z1) by A2,Th41;
A7: Im2 (-(z2 - z1)) = -(Im2 z2 - Im2 z1) by A3,Th41;
A8: Im3 (-(z2 - z1)) = -(Im3 z2 - Im3 z1) by A4,Th41;
A9: Rea (z1 - z2) = Rea z1 - Rea z2 by Th42;
A10: Im1 (z1 - z2) = Im1 z1 - Im1 z2 by Th42;
A11: Im2 (z1 - z2) = Im2 z1 - Im2 z2 by Th42;
  Im3 (z1 - z2) = Im3 z1 - Im3 z2 by Th42;
  hence thesis by Th25,A9,A10,A11,A5,A6,A7,A8;
end;

Lm39: z1 - z2 = 0 implies z1 = z2
proof
  assume
A1: z1 - z2 = 0;
A2: Rea (z1 - z2) = Rea z1 - Rea z2 by Th42;
A3: Im1 (z1 - z2) = Im1 z1 - Im1 z2 by Th42;
A4: Im2 (z1 - z2) = Im2 z1 - Im2 z2 by Th42;
A5: Im3 (z1 - z2) = Im3 z1 - Im3 z2 by Th42;
A6: Rea (z1 - z2) = 0 by A1,Lm7,Th23;
A7: Im1 (z1 - z2) = 0 by A1,Lm7,Th23;
A8: Im2 (z1 - z2) = 0 by A1,Lm7,Th23;
  Im3 (z1 - z2) = 0 by A1,Lm7,Th23;
  hence thesis by A2,A3,A4,A5,A6,A7,A8,Th25;
end;

theorem
  |.z1.| - |.z2.| <= |.z1 + z2.|
proof z1 = z1 + z2 - z2 by Lm35;
  then |.z1.| <= |.z1 + z2.| + |.z2.| by Th80;
  hence thesis by XREAL_1:20;
end;

theorem Th82:
  |.z1.| - |.z2.| <= |.z1 - z2.|
proof z1 = z1 - z2 + z2 by Lm36;
  then |.z1.| <= |.z1 - z2.| + |.z2.| by Th79;
  hence thesis by XREAL_1:20;
end;

theorem Th83:
  |.z1 - z2.| = |.z2 - z1.|
proof
  thus |.z1 - z2.| = |.-(z2 - z1).| by Lm38
    .= |.z2 - z1.| by Th72;
end;

theorem
  |.z1 - z2.| = 0 iff z1 = z2
proof
  thus |.z1 - z2.| = 0 implies z1 = z2 by Lm39,Th66;
  assume z1 = z2; then
  z1 - z2 = [*Rea z1-Rea z1, Im1 z1-Im1 z1, Im2 z1-Im2 z1, Im3 z1-Im3 z1*]
    by Lm37
    .= 0 by Lm7;
  hence thesis by Th65;
end;

Lm40: for z,z1,z2 being quaternion number holds z1-z2 = (z1 - z) + (z - z2)
proof
  let z,z1,z2 be quaternion number;
A1: Rea ((z1 - z) + (z - z2)) = Rea (z1 - z) + Rea (z - z2) by Lm13
    .= Rea (z1 - z) + (Rea z - Rea z2) by Th42
    .= (Rea z1 - Rea z) + (Rea z - Rea z2) by Th42
    .= Rea z1 - Rea z2
    .= Rea (z1 - z2) by Th42;
A2: Im1 ((z1 - z) + (z - z2)) = Im1 (z1 - z) + Im1 (z - z2) by Lm13
    .= Im1 (z1 - z) + (Im1 z - Im1 z2) by Th42
    .= (Im1 z1 - Im1 z) + (Im1 z - Im1 z2) by Th42
    .= Im1 z1 - Im1 z2
    .= Im1 (z1 - z2) by Th42;
A3: Im2 ((z1 - z) + (z - z2)) = Im2 (z1 - z) + Im2 (z - z2) by Lm13
    .= Im2 (z1 - z) + (Im2 z - Im2 z2) by Th42
    .= (Im2 z1 - Im2 z) + (Im2 z - Im2 z2) by Th42
    .= Im2 z1 - Im2 z2
    .= Im2 (z1 - z2) by Th42;
  Im3 ((z1 - z) + (z - z2)) = Im3 (z1 - z) + Im3 (z - z2) by Lm13
    .= Im3 (z1 - z) + (Im3 z - Im3 z2) by Th42
    .= (Im3 z1 - Im3 z) + (Im3 z - Im3 z2) by Th42
    .= Im3 z1 - Im3 z2
    .= Im3 (z1 - z2) by Th42;
  hence thesis by A1,A2,A3,Th25;
end;

theorem
  |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
  |.z1 - z2.| = |.(z1 - z) + (z - z2).| by Lm40;
  hence thesis by Th79;
end;

theorem
  |.|.z1.| - |.z2.|.| <= |.z1 - z2.|
proof
  |.z2.| - |.z1.| <= |.z2 - z1.| by Th82;
  then -(|.z1.| - |.z2.|) <= |.z1 - z2.| by Th83; then
A1: -|.z1 - z2.| <= --(|.z1.| - |.z2.|) by XREAL_1:24;
  |.z1.| - |.z2.| <= |.z1 - z2.| by Th82;
  hence thesis by A1,ABSVALUE:5;
end;

theorem Th87:
  |.z1*z2.| = |.z1.|*|.z2.|
proof
  set m1 = Rea z1, m2 = Im1 z1, m3 = Im2 z1, m4 = Im3 z1,
  n1 = Rea z2, n2 = Im1 z2, n3 = Im2 z2, n4 = Im3 z2;
A1: Rea (z1 * z2) = m1*n1 - m2*n2 - m3*n3 - m4*n4 by Lm18;
A2: Im1 (z1 * z2) = m1*n2 + m2*n1 + m3*n4 - m4*n3 by Lm18;
A3: Im2 (z1 * z2) = m1*n3 + m3*n1 + m4*n2 - m2*n4 by Lm18;
A4: Im3 (z1 * z2) = m1*n4 + m4*n1 + m2*n3 - m3*n2 by Lm18;
  set b1=m1*n1 - m2*n2 - m3*n3 - m4*n4, b2 = m1*n2 + m2*n1 + m3*n4 - m4*n3,
  b3 = m1*n3 + m3*n1 + m4*n2 - m2*n4, b4 = m1*n4 + m4*n1 + m2*n3 - m3*n2;
A5: (m1^2 + m2^2 + m3^2 + m4^2)>=0 by Th74;
A6: (n1^2 + n2^2 + n3^2 + n4^2) >= 0 by Th74;
  sqrt(b1^2 +b2^2 +b3^2 +b4^2)
  =sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2));
  hence thesis by A1,A2,A3,A4,A5,A6,SQUARE_1:29;
end;

theorem
  |.z*z.| = (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2
proof
A1: (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2 >= 0 by Th74;
  |.z.| * |.z.| =(sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2))^2
    .= (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2 by A1,SQUARE_1:def 2;
  hence thesis by Th87;
end;

theorem
  |.z*z.| = |.z*z*'.|
proof
  thus |.z*z.| = |.z.|*|.z.| by Th87
    .= |.z.|*|.z*'.| by Th73
    .= |.z*z*'.| by Th87;
end;

theorem
  z is real implies Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0
proof
  assume z is real;
  then z in REAL by XREAL_0:def 1;
  hence thesis by Lm19;
end;

theorem
  for x,y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm4;

theorem
  z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)*<i> +
    (Im2 z1 + Im2 z2)*<j> + (Im3 z1 + Im3 z2)*<k> by Lm21;

theorem
  z1*z2 =
  (Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
  (Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
  (Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2)*<j> +
  (Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
    by Lm22;

theorem
  -z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm25;

theorem
  z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
    (Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Lm26;

theorem
  for a, b, c, d being real number st a^2 + b^2 + c^2 + d^2 = 0 holds
    a = 0 & b = 0 & c = 0 & d = 0 by Lm10;

theorem
Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
  by Lm18;