:: Groups
::  by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990-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, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2,
      RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1,
      SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1,
      TARSKI, RLVECT_1, SUPINF_2, GROUP_1;
 notations TARSKI, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
      RELAT_1, FUNCT_1, REAL_1, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0, ALGSTR_0,
      RLVECT_1, INT_1, ORDINAL1, NAT_1, FINSEQOP, SETWISEO, INT_2;
 constructors BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2,
      FINSEQOP, RLVECT_1, SEQ_1;
 registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
      INT_1, STRUCT_0, XBOOLE_0, ALGSTR_0, CARD_1, REAL_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions FUNCT_2, BINOP_1, FINSEQOP, STRUCT_0, RLVECT_1, SETWISEO,
      ALGSTR_0;
 theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2,
      XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D;
 schemes FUNCT_2, INT_1, NAT_1, BINOP_1, CLASSES1;

begin

reserve m,n for Nat;
reserve i,j for Integer;
reserve S for non empty multMagma;
reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S;

Lm1: now
  set G = multMagma (# REAL, addreal #);
  thus for h,g,f being Element of G holds h * g * f = h * (g * f)
  proof
    let h,g,f be Element of G;
    reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
    h * g = A + B by BINOP_2:def 9;
    hence h * g * f = A + B + C by BINOP_2:def 9
      .= A + (B + C)
      .= h * (g * f) by A1,BINOP_2:def 9;
  end;
  reconsider e = 0 as Element of G;
  take e;
  let h be Element of G;
  reconsider A = h as Real;
  thus h * e = A + 0 by BINOP_2:def 9
    .= h;
  thus e * h = 0 + A by BINOP_2:def 9
    .= h;
  reconsider g = - A as Element of G;
  take g;
  thus h * g = A + (- A) by BINOP_2:def 9
    .= e;
  thus g * h = (- A) + A by BINOP_2:def 9
    .= e;
end;

definition
  let IT be multMagma;

  attr IT is unital means
  :Def1:
  ex e being Element of IT st for h being
  Element of IT holds h * e = h & e * h = h;
  attr IT is Group-like means
  :Def2:
  ex e being Element of IT st for h being
Element of IT holds h * e = h & e * h = h & ex g being Element of IT st h * g =
  e & g * h = e;
  attr IT is associative means
  :Def3:
  for x,y,z being Element of IT holds (x*y )*z = x*(y*z);
end;

registration
  cluster Group-like -> unital for multMagma;
  coherence
  proof
    let IT be multMagma;
    assume ex e being Element of IT st for h being Element of IT holds h * e
    = h & e * h = h & ex g being Element of IT st h * g = e & g * h = e;
    hence
    ex e being Element of IT st for h being Element of IT holds h * e = h
    & e * h = h;
  end;
end;

registration
  cluster strict Group-like associative non empty for multMagma;
  existence
  proof
    multMagma (# REAL, addreal #) is Group-like associative by Def2,Def3,Lm1;
    hence thesis;
  end;
end;

definition
  mode Group is Group-like associative non empty multMagma;
end;

theorem
  ((for r,s,t holds (r * s) * t = r * (s * t)) & ex t st for s1 holds s1
* t = s1 & t * s1 = s1 & ex s2 st s1 * s2 = t & s2 * s1 = t) implies S is Group
  by Def2,Def3;

theorem
  (for r,s,t holds r * s * t = r * (s * t)) & (for r,s holds (ex t st r
  * t = s) & (ex t st t * r = s)) implies S is associative Group-like
proof
  set r = the Element of S;
  assume that
A1: for r,s,t holds r * s * t = r * (s * t) and
A2: for r,s holds (ex t st r * t = s) & ex t st t * r = s;
  consider s1 such that
A3: r * s1 = r by A2;
  thus for r,s,t holds r * s * t = r * (s * t) by A1;
  take s1;
  let s;
  ex t st t * r = s by A2;
  hence
A4: s * s1 = s by A1,A3;
  consider s2 such that
A5: s2 * r = r by A2;
  consider t1 such that
A6: r * t1 = s1 by A2;
A7: ex t2 st t2 * r = s2 by A2;
A8: s1 = s2 * (r * t1) by A1,A5,A6
    .= s2 by A1,A3,A6,A7;
  ex t st r * t = s by A2;
  hence
A9: s1 * s = s by A1,A5,A8;
  consider t1 such that
A10: s * t1 = s1 by A2;
  consider t2 such that
A11: t2 * s = s1 by A2;
  take t1;
  consider r1 such that
A12: s * r1 = t1 by A2;
A13: ex r2 st r2 * s = t2 by A2;
  t1 = s1 * (s * r1) by A1,A9,A12
    .= t2 * (s * t1) by A1,A11,A12
    .= t2 by A1,A4,A10,A13;
  hence thesis by A10,A11;
end;

theorem Th3:
  multMagma (# REAL, addreal #) is associative Group-like
proof
  set G = multMagma (# REAL, addreal #);
  thus for h,g,f being Element of G holds h * g * f = h * (g * f)
  proof
    let h,g,f be Element of G;
    reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
    h * g = A + B by BINOP_2:def 9;
    hence h * g * f = A + B + C by BINOP_2:def 9
      .= A + (B + C)
      .= h * (g * f) by A1,BINOP_2:def 9;
  end;
  reconsider e = 0 as Element of G;
  take e;
  let h be Element of G;
  reconsider A = h as Real;
  thus h * e = A + 0 by BINOP_2:def 9
    .= h;
  thus e * h = 0 + A by BINOP_2:def 9
    .= h;
  reconsider g = - A as Element of G;
  take g;
  thus h * g = A + (- A) by BINOP_2:def 9
    .= e;
  thus g * h = (- A) + A by BINOP_2:def 9
    .= e;
end;

reserve G for Group-like non empty multMagma;
reserve e,h for Element of G;

definition
  let G be multMagma such that
A1: G is unital;
  func 1_G -> Element of G means
  :Def4:
  for h being Element of G holds h * it = h & it * h = h;
  existence by A1,Def1;
  uniqueness
  proof
    let e1,e2 be Element of G;
    assume that
A1: for h being Element of G holds h * e1 = h & e1 * h = h and
A2: for h being Element of G holds h * e2 = h & e2 * h = h;
    thus e1 = e2 * e1 by A2
      .= e2 by A1;
  end;
end;

theorem
  (for h holds h * e = h & e * h = h) implies e = 1_G by Def4;

reserve G for Group;
reserve f,g,h for Element of G;

definition
  let G,h;
  func h" -> Element of G means
  :Def5:
  h * it = 1_G & it * h = 1_G;
  existence
  proof
    consider e being Element of G such that
A1: for h being Element of G holds h * e = h & e * h = h & ex g being
    Element of G st h * g = e & g * h = e by Def2;
    consider g being Element of G such that
A2: h * g = e & g * h = e by A1;
    take g;
    thus thesis by A1,A2,Def4;
  end;
  uniqueness
  proof
    let h1,h2 be Element of G;
    assume that
A3: h * h1 = 1_G and
    h1 * h = 1_G and
    h * h2 = 1_G and
A4: h2 * h = 1_G;
    thus h1 = 1_G * h1 by Def4
      .= h2 * (h * h1) by A4,Def3
      .= h2 by A3,Def4;
  end;
  involutiveness;
end;

theorem
  h * g = 1_G & g * h = 1_G implies g = h" by Def5;

theorem Th6:
  h * g = h * f or g * h = f * h implies g = f
proof
  assume h * g = h * f or g * h = f * h;
  then h" * (h * g) = h" * h * f or g * h * h" = f * (h * h") by Def3;
  then h" * (h * g) = 1_G * f or g * (h * h") = f * (h * h") by Def3,Def5;
  then h" * (h * g) = f or g * 1_G = f * (h * h") by Def4,Def5;
  then h" * h * g = f or g = f * (h * h") by Def3,Def4;
  then h" * h * g = f or g = f * 1_G by Def5;
  then 1_G * g = f or g = f by Def4,Def5;
  hence thesis by Def4;
end;

theorem
  h * g = h or g * h = h implies g = 1_G
proof
  h * 1_G = h & 1_G * h = h by Def4;
  hence thesis by Th6;
end;

theorem Th8:
  (1_G)" = 1_G
proof
  (1_G)" * 1_G = 1_G by Def5;
  hence thesis by Def4;
end;

theorem
  h" = g" implies h = g
proof
  assume h" = g";
  then
A1: h * g" = 1_G by Def5;
  g * g" = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem
  h" = 1_G implies h = 1_G
proof
  (1_G)" = 1_G by Th8;
  hence thesis;
end;

canceled;

theorem Th12:
  h * g = 1_G implies h = g" & g = h"
proof
  assume
A1: h * g = 1_G;
  h * h" = 1_G & g" * g = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem Th13:
  h * f = g iff f = h" * g
proof
  h * (h" * g) = h * h" * g by Def3
    .= 1_G * g by Def5
    .= g by Def4;
  hence h * f = g implies f = h" * g by Th6;
  assume f = h" * g;
  hence h * f = h * h" * g by Def3
    .= 1_G * g by Def5
    .= g by Def4;
end;

theorem Th14:
  f * h = g iff f = g * h"
proof
  g * h" * h = g * (h" * h) by Def3
    .= g * 1_G by Def5
    .= g by Def4;
  hence f * h = g implies f = g * h" by Th6;
  assume f = g * h";
  hence f * h = g * (h" * h) by Def3
    .= g * 1_G by Def5
    .= g by Def4;
end;

theorem
  ex f st g * f = h
proof
  take g" * h;
  thus thesis by Th13;
end;

theorem
  ex f st f * g = h
proof
  take h * g";
  thus thesis by Th14;
end;

theorem Th17:
  (h * g)" = g" * h"
proof
  (g" * h") * (h * g) = g" * h" * h * g by Def3
    .= g" * (h" * h) * g by Def3
    .= g" * 1_G * g by Def5
    .= g" * g by Def4
    .= 1_G by Def5;
  hence thesis by Th12;
end;

theorem Th18:
  g * h = h * g iff (g * h)" = g" * h"
proof
  thus g * h = h * g implies (g * h)" = g" * h" by Th17;
  assume (g * h)" = g" * h";
  then
A1: (h * g) * (g * h)" = h * g * g" * h" by Def3
    .= h * (g * g") * h" by Def3
    .= h * 1_G * h" by Def5
    .= h * h" by Def4
    .= 1_G by Def5;
  (g * h) * (g * h)" = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem Th19:
  g * h = h * g iff g" * h" = h" * g"
proof
  thus g * h = h * g implies g" * h" = h" * g"
  proof
    assume
A1: g * h = h * g;
    hence g" * h" = (g * h)" by Th17
      .= h" * g" by A1,Th18;
  end;
  assume
A2: g" * h" = h" * g";
  thus g * h = (g * h)"" .= (h" * g")" by Th17
    .= h"" * g"" by A2,Th17
    .= h * g;
end;

theorem Th20:
  g * h = h * g iff g * h" = h" * g
proof
  thus g * h = h * g implies g * h" = h" * g
  proof
    assume
A1: g * h = h * g;
    (g * h") * (g" * h) = g * h" * g" * h by Def3
      .= g * (h" * g") * h by Def3
      .= g * (g" * h") * h by A1,Th19
      .= g * g" * h" * h by Def3
      .= 1_G * h" * h by Def5
      .= h" * h by Def4
      .= 1_G by Def5;
    then g * h" = (g" * h)" by Th12
      .= h" * g"" by Th17;
    hence thesis;
  end;
  assume g * h" = h" * g;
  then g * (h" * h) = h" * g * h by Def3;
  then g * 1_G = h" * g * h by Def5;
  then g = h" * g * h by Def4;
  then g = h" * (g * h) by Def3;
  then h * g = h * h" * (g * h) by Def3;
  then h * g = 1_G * (g * h) by Def5;
  hence thesis by Def4;
end;

reserve u for UnOp of G;

definition
  let G;
  func inverse_op(G) -> UnOp of G means
  :Def6:
  it.h = h";
  existence
  proof
    deffunc F(Element of G) = $1";
    consider u such that
A1: for h being Element of G holds u.h = F(h) from FUNCT_2:sch 4;
    take u;
    let h;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let u1,u2 be UnOp of G;
    assume
A2: for h holds u1.h = h";
    assume
A3: for h holds u2.h = h";
    let h be Element of G;
    thus u1.h = h" by A2
      .= u2.h by A3;
  end;
end;

registration
  let G be associative non empty multMagma;
  cluster  the multF of G -> associative;
  coherence
proof
  let h,g,f be Element of G;
  set o = the multF of G;
  thus o.(h,o.(g,f)) = h * (g * f) .= h * g * f by Def3
    .= o.(o.(h,g),f);
end;
end;

theorem Th21:
  for G being unital non empty multMagma holds 1_G is_a_unity_wrt
  the multF of G
proof
  let G be unital non empty multMagma;
  set o = the multF of G;
  now
    let h be Element of G;
    thus o.(1_G,h) = 1_G * h .= h by Def4;
    thus o.(h,1_G) = h * 1_G .= h by Def4;
  end;
  hence thesis by BINOP_1:3;
end;

theorem Th22:
  for G being unital non empty multMagma holds the_unity_wrt the
  multF of G = 1_G
proof
  let G be unital non empty multMagma;
  1_G is_a_unity_wrt the multF of G by Th21;
  hence thesis by BINOP_1:def 8;
end;

registration
  let G be unital non empty multMagma;
  cluster the multF of G -> having_a_unity;
coherence
proof
  take 1_G;
  thus thesis by Th21;
end;
end;

theorem Th23:
  inverse_op(G) is_an_inverseOp_wrt the multF of G
proof
  let h be Element of G;
  thus (the multF of G).(h,inverse_op(G).h) = h * h" by Def6
    .= 1_G by Def5
    .= the_unity_wrt the multF of G by Th22;
  thus (the multF of G).(inverse_op(G).h,h) = h" * h by Def6
    .= 1_G by Def5
    .= the_unity_wrt the multF of G by Th22;
end;

registration
  let G;
  cluster the multF of G -> having_an_inverseOp;
  coherence
proof
  inverse_op(G) is_an_inverseOp_wrt the multF of G by Th23;
  hence thesis by FINSEQOP:def 2;
end;
end;

theorem
  the_inverseOp_wrt the multF of G = inverse_op(G)
proof
  set o = the multF of G;
  o is having_an_inverseOp & inverse_op(G) is_an_inverseOp_wrt o by Th23;
  hence thesis by FINSEQOP:def 3;
end;

definition
  let G be non empty multMagma;
  func power G -> Function of [:the carrier of G,NAT:], the carrier of G means
  :Def7:
  for h being Element of G holds it.(h,0) = 1_G & for n being Element of
  NAT holds it.(h,n + 1) = it.(h,n) * h;
  existence
  proof
    defpred P[set,set] means ex g0 being Function of NAT, the carrier of G, h
being Element of G st $1 = h & g0 = $2 & g0.0 = 1_G & for n holds g0.(n + 1) =
    (g0.n) * h;
A1: for x be set st x in the carrier of G ex y be set st P[x,y]
    proof
      let x be set;
      assume x in the carrier of G;
      then reconsider b = x as Element of G;
      deffunc F(Nat,Element of G) = $2 * b;
      consider g0 being Function of NAT, the carrier of G such that
A2:   g0.0 = 1_G and
A3:   for n being Nat holds g0.(n + 1) = F(n,g0.n) from NAT_1:sch 12;
      reconsider y = g0 as set;
      take y;
      take g0;
      take b;
      thus x = b & g0 = y & g0.0 = 1_G by A2;
      let n;
      thus thesis by A3;
    end;
    consider f being Function such that
    dom f = the carrier of G and
A4: for x be set st x in the carrier of G holds P[x,f.x] from CLASSES1
    :sch 1(A1);
    defpred P[Element of G,Element of NAT,set] means ex g0 being Function of
    NAT, the carrier of G st g0 = f.$1 & $3 = g0.$2;
A5: for a being Element of G, n being Element of NAT ex b being Element of
    G st P[a,n,b]
    proof
      let a be Element of G, n be Element of NAT;
      consider g0 being Function of NAT, the carrier of G, h being Element of
      G such that
      a = h and
A6:   g0 = f.a and
      g0.0 = 1_G and
      for n holds g0.(n + 1) = (g0.n) * h by A4;
      take g0.n, g0;
      thus thesis by A6;
    end;
    consider F being Function of [:the carrier of G,NAT:], the carrier of G
    such that
A7: for a being Element of G, n being Element of NAT holds P[a,n,F.(a,
    n)] from BINOP_1:sch 3 (A5);
    take F;
    let h be Element of G;
A8: ex g2 being Function of NAT, the carrier of G, b being Element of G
st h = b & g2 = f.h & g2.0 = 1_G & for n holds g2.(n + 1) = (g2.n) * b by A4;
    ex g1 being Function of NAT, the carrier of G st g1 = f.h & F.(h,0) =
    g1.0 by A7;
    hence F.(h,0) = 1_G by A8;
    let n be Element of NAT;
A9: ex g2 being Function of NAT, the carrier of G, b being Element of G st
    h = b & g2 = f.h & g2.0 = 1_G & for n holds g2.(n + 1) = ( g2.n) * b by A4;
    ( ex g0 being Function of NAT, the carrier of G st g0 = f.h & F.(h,n)
= g0.n)& ex g1 being Function of NAT, the carrier of G st g1 = f.h & F.(h,n + 1
    ) = g1.(n + 1) by A7;
    hence thesis by A9;
  end;
  uniqueness
  proof
    let f,g be Function of [:the carrier of G,NAT:], the carrier of G;
    assume that
A10: for h being Element of G holds f.(h,0) = 1_G & for n being
    Element of NAT holds f.(h,n + 1) = (f.(h,n)) * h and
A11: for h being Element of G holds g.(h,0) = 1_G & for n being
    Element of NAT holds g.(h,n + 1) = (g.(h,n)) * h;
    now
      let h be Element of G, n be Element of NAT;
      defpred P[Nat] means f.[h,$1] = g.[h,$1];
A12:  now
        let n be Element of NAT;
        assume
A13:    P[n];
A14:    g.[h,n] = g.(h,n);
        f.[h,n + 1] = f.(h,n + 1) .= (f.(h,n)) * h by A10
          .= g.(h,n + 1) by A11,A13,A14
          .= g.[h,n + 1];
        hence P[n+1];
      end;
      f.[h,0] = f.(h,0) .= 1_G by A10
        .= g.(h,0) by A11
        .= g.[h,0];
      then
A15:  P[0];
      for n being Element of NAT holds P[n] from NAT_1:sch 1(A15,A12);
      hence f.(h,n) = g.(h,n);
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let G,i,h;
  func h |^ i -> Element of G equals
  :Def8:
  power(G).(h,abs(i)) if 0 <= i
  otherwise (power(G).(h,abs(i)))";
  correctness;
end;

definition
  let G,n,h;
  redefine func h |^ n equals
  power(G).(h,n);
  compatibility
  proof
    let g be Element of G;
    abs(n) = n by ABSVALUE:def 1;
    hence thesis by Def8;
  end;
end;

Lm2: h |^ (n + 1) = h |^ n * h
proof
  reconsider n as Element of NAT by ORDINAL1:def 12;
  h |^ (n + 1) = h |^ n * h by Def7;
  hence thesis;
end;

Lm3: h |^ 0 = 1_G by Def7;

Lm4: (1_G) |^ n = 1_G
proof
  defpred P[Nat] means (1_G) |^ $1 = 1_G;
A1: now
    let n;
    assume P[n];
    then (1_G) |^ (n + 1) = 1_G * 1_G by Lm2
      .= 1_G by Def4;
    hence P[n+1];
  end;
A2: P[0] by Def7;
  for n holds P[n] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

theorem
  h |^ 0 = 1_G by Def7;

theorem Th26:
  h |^ 1 = h
proof
  thus h |^ 1 = h |^(0 + 1) .= h |^ 0 * h by Lm2
    .= 1_G * h by Def7
    .= h by Def4;
end;

theorem Th27:
  h |^ 2 = h * h
proof
  thus h |^ 2 = h |^ (1 + 1) .= h |^ 1 * h by Lm2
    .= h * h by Th26;
end;

theorem
  h |^ 3 = h * h * h
proof
  thus h |^ 3 = h |^ (2 + 1) .= h |^ 2 * h by Lm2
    .= h * h * h by Th27;
end;

theorem
  h |^ 2 = 1_G iff h" = h
proof
  thus h |^ 2 = 1_G implies h = h"
  proof
    assume h |^ 2 = 1_G;
    then h * h = 1_G by Th27;
    hence thesis by Th12;
  end;
  assume h = h";
  hence h |^ 2 = h * h" by Th27
    .= 1_G by Def5;
end;

Lm5: h |^ (n + m) = h |^ n * (h |^ m)
proof
  defpred P[Nat] means for n holds h |^ (n + $1) = h |^ n * (h |^ $1);
A1: for m st P[m] holds P[m+1]
  proof
    let m;
    assume
A2: for n holds h |^ (n + m) = h |^ n * (h |^ m);
    let n;
    thus h |^ (n + (m + 1)) = h |^ (n + m + 1) .= h |^ (n + m) * h by Lm2
      .= h |^ n * (h |^ m) * h by A2
      .= h |^ n * (h |^ m * h) by Def3
      .= h |^ n * (h |^ (m + 1)) by Lm2;
  end;
A3: P[0]
  proof
    let n;
    thus h |^ (n + 0) = h |^ n * 1_G by Def4
      .= h |^ n * (h |^ 0) by Def7;
  end;
  for m holds P[m] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm6: h |^ (n + 1) = h |^ n * h & h |^ (n + 1) = h * (h |^ n)
proof
  thus h |^ (n + 1) = h |^ n * h by Lm2;
  thus h |^ (n + 1) = h |^ 1 * (h |^ n) by Lm5
    .= h * (h |^ n) by Th26;
end;

Lm7: h |^ (n * m) = h |^ n |^ m
proof
  defpred P[Nat] means for n holds h |^ (n * $1) = h |^ n |^ $1;
A1: for m st P[m] holds P[m+1]
  proof
    let m;
    assume
A2: for n holds h |^ (n * m) = h |^ n |^ m;
    let n;
    thus h |^ (n * (m + 1)) = h |^ (n * m + n * 1)
      .= h |^ (n * m) * (h |^ n) by Lm5
      .= h |^ n |^ m * (h |^ n) by A2
      .= h |^ n |^ m * (h |^ n |^ 1) by Th26
      .= h |^ n |^ (m + 1) by Lm5;
  end;
A3: P[0]
  proof
    let n;
    thus h |^ (n * 0) = 1_G by Def7
      .= h |^ n |^ 0 by Def7;
  end;
  for m holds P[m] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm8: h" |^ n = (h |^ n)"
proof
  defpred P[Nat] means h" |^ $1 = (h |^ $1)";
A1: now
    let n;
    assume P[n];
    then h" |^ (n + 1) = (h |^ n)" * h" by Lm2
      .= (h * (h |^ n))" by Th17
      .= (h |^ (n + 1))" by Lm6;
    hence P[n+1];
  end;
  h" |^ 0 = 1_G by Def7
    .= (1_G)" by Th8
    .= (h |^ 0)" by Def7;
  then
A2: P[0];
  for n holds P[n] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

Lm9: g * h = h * g implies g * (h |^ n) = h |^ n * g
proof
  defpred P[Nat] means g * h = h * g implies g * (h |^ $1) = h |^ $1 * g;
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: g * h = h * g implies g * (h |^ n) = h |^ n * g;
    assume
A3: g * h = h * g;
    thus g * (h |^ (n + 1)) = g * (h * (h |^ n)) by Lm6
      .= g * h * (h |^ n) by Def3
      .= h * ((h |^ n) * g)by A2,A3,Def3
      .= h * (h |^ n) * g by Def3
      .= h |^ (n + 1) * g by Lm6;
  end;
A4: P[0]
  proof
    assume g * h = h * g;
    thus g * (h |^ 0) = g * 1_G by Def7
      .= g by Def4
      .= 1_G * g by Def4
      .= h |^ 0 * g by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

Lm10: g * h = h * g implies g |^ n * (h |^ m) = h |^ m * (g |^ n)
proof
  defpred P[Nat] means for m st g * h = h * g holds g |^ $1 * (h |^ m) = h |^
  m * (g |^ $1);
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: for m st g * h = h * g holds g |^ n * (h |^ m) = h |^ m * (g |^ n);
    let m;
    assume
A3: g * h = h * g;
    thus g |^ (n + 1) * (h |^ m) = g * (g |^ n) * (h |^ m) by Lm6
      .= g * ((g |^ n) * (h |^ m)) by Def3
      .= g * ((h |^ m) * (g |^ n)) by A2,A3
      .= g * (h |^ m) * (g |^ n) by Def3
      .= h |^ m * g * (g |^ n) by A3,Lm9
      .= h |^ m * (g * (g |^ n)) by Def3
      .= h |^ m * (g |^ (n + 1)) by Lm6;
  end;
A4: P[0]
  proof
    let m;
    assume g * h = h * g;
    thus g |^ 0 * (h |^ m) = 1_G * (h |^ m)by Def7
      .= h |^ m by Def4
      .= h |^ m * 1_G by Def4
      .= h |^ m * (g |^ 0) by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

Lm11: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n)
proof
  defpred P[Nat] means g * h = h * g implies (g * h) |^ $1 = g |^ $1 * (h |^
  $1);
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n);
    assume
A3: g * h = h * g;
    hence (g * h) |^ (n + 1) = g |^ n * (h |^ n) * (h * g) by A2,Lm6
      .= g |^ n * (h |^ n) * h * g by Def3
      .= g |^ n * ((h |^ n) * h) * g by Def3
      .= g |^ n * (h |^ (n + 1)) * g by Lm6
      .= h |^ (n + 1) * (g |^ n) * g by A3,Lm10
      .= h |^ (n + 1) * ((g |^ n) * g) by Def3
      .= h |^ (n + 1) * (g |^ (n + 1)) by Lm6
      .= g |^ (n + 1) * (h |^ (n + 1)) by A3,Lm10;
  end;
A4: P[0]
  proof
    assume g * h = h * g;
    thus (g * h) |^ 0 = 1_G by Def7
      .= 1_G * 1_G by Def4
      .= g |^ 0 * 1_G by Def7
      .= g |^ 0 * (h |^ 0) by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

theorem Th30:
  i <= 0 implies h |^ i = (h |^ abs(i))"
proof
  assume
A1: i <= 0;
  per cases by A1;
  suppose
    i < 0;
    hence thesis by Def8;
  end;
  suppose
A2: i = 0;
    hence h |^ i = 1_G by Lm3
      .= (1_G)" by Th8
      .= (h |^ 0)" by Def7
      .= (h |^ abs(i))" by A2,ABSVALUE:def 1;
  end;
end;

theorem
  (1_G) |^ i = 1_G
proof
  (1_G) |^ i = (1_G) |^ abs(i) or (1_G) |^ i = ((1_G) |^ abs(i))" & (1_G)"
  = 1_G by Def8,Th8;
  hence thesis by Lm4;
end;

theorem Th32:
  h |^ (-1) = h"
proof
  abs( - 1 ) = - (-1) by ABSVALUE:def 1;
  hence h |^ (-1) = (h |^ 1)" by Def8
    .= h" by Th26;
end;

Lm12: h |^ (- i) = (h |^ i)"
proof
  per cases;
  suppose
A1: i >= 0;
    per cases by A1,XREAL_1:24;
    suppose
A2:   - i < -0;
      hence h |^ (- i) = (h |^ abs( - i ))" by Def8
        .= (h |^ (- (- i)))" by A2,ABSVALUE:def 1
        .= (h |^ i)";
    end;
    suppose
A3:   i = 0;
      hence h |^ (- i) = 1_G by Lm3
        .= (1_G)" by Th8
        .= (h |^ i)" by A3,Lm3;
    end;
  end;
  suppose
A4: i < 0;
    then h |^ i = (h |^ abs(i))" by Def8;
    hence thesis by A4,ABSVALUE:def 1;
  end;
end;

Lm13: j >= 1 or j = 0 or j < 0
proof
  j < 0 or j is Element of NAT & (j <> 0 or j = 0) by INT_1:3;
  hence thesis by NAT_1:14;
end;

Lm14: h |^ (j - 1) = h |^ j * (h |^ (-1))
proof
A1: now
    per cases by Lm13;
    suppose
A2:   j >= 1;
      then j >= 1 + 0;
      then
A3:   j - 1 >= 0 by XREAL_1:19;
      then
A4:   abs( j - 1 ) + 1 = j - 1 + 1 by ABSVALUE:def 1
        .= j;
A5:   abs j = j by A2,ABSVALUE:def 1;
A6:   abs j = abs(-j) by COMPLEX1:52;
      thus h|^(j - 1) * (h * (h|^(- j))) = h|^(j - 1) * h * (h|^(- j)) by Def3
        .= h |^ abs( j - 1 ) * h * (h |^ (- j)) by A3,Def8
        .= h |^ abs( j - 1 ) * h * ((h |^ abs( - j ))") by A2,Th30
        .= h |^ (abs( j - 1 ) + 1) * ((h |^ abs( - j ))") by Lm6
        .= 1_G by A4,A5,A6,Def5;
    end;
    suppose
A7:   j < 0;
A8:   1 - j = - (j - 1);
      thus h |^ (j - 1) * (h * (h |^ (- j))) = (h |^ abs( j - 1 ))" * (h * (h
      |^ (- j))) by A7,Def8
        .= (h |^ abs( j - 1 ))" * (h * (h |^ abs( - j ))) by A7,Def8
        .= (h |^ abs( j - 1 ))" * (h |^ (1 + abs( - j ))) by Lm6
        .= (h |^ abs( j - 1 ))" * (h |^ (1 + (- j))) by A7,ABSVALUE:def 1
        .= (h |^ abs( j - 1 ))" * (h |^ abs( j - 1 )) by A7,A8,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
A9:   j = 0;
      hence h |^ (j - 1) * (h * (h |^ (- j))) = h" * (h * (h |^ (- j))) by Th32
        .= h " * h * (h |^ (- j)) by Def3
        .= 1_G * (h |^ (- j)) by Def5
        .= h |^ 0 by A9,Def4
        .= 1_G by Def7;
    end;
  end;
  h|^(j - 1) * (h|^(1 - j)) = h|^(j - 1) * (h|^(- (j - 1)))
    .= h |^ (j - 1) * (h |^ (j - 1))" by Lm12
    .= 1_G by Def5;
  then h * (h |^ (- j)) = h |^ (1 - j) by A1,Th6;
  then (h |^ (1 - j))" = (h |^ (- j))" * h" by Th17
    .= (h |^ (- (- j))) * h" by Lm12
    .= h |^ j * (h |^ (-1)) by Th32;
  then h |^ j * (h |^ (-1)) = h |^ (- (1 - j)) by Lm12;
  hence thesis;
end;

Lm15: j >= 0 or j = - 1 or j < - 1
proof
  per cases;
  suppose
    j >= 0;
    hence thesis;
  end;
  suppose
A1: j < 0;
    then reconsider n = - j as Element of NAT by INT_1:3;
    n <> -0 by A1;
    then n >= 1 by NAT_1:14;
    then n > 1 or n = 1 by XXREAL_0:1;
    then - 1 > - (- j) or - 1 = j by XREAL_1:24;
    hence thesis;
  end;
end;

Lm16: h |^ (j + 1) = h |^ j * (h |^ 1)
proof
A1: now
    per cases by Lm15;
    suppose
A2:   j >= 0;
      then reconsider n = j as Element of NAT by INT_1:3;
A3:   n + 1 = abs( j + 1 ) by ABSVALUE:def 1;
      n + 1 >= 0;
      hence
      h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = h |^ abs( j + 1 ) * (
      (h |^ (-1)) * (h |^ (- j))) by Def8
        .= h |^ abs( j + 1 ) * (h" * (h |^ (- j))) by Th32
        .= h |^ abs( j + 1 ) * (h" * (h |^ j)") by Lm12
        .= h |^ abs( j + 1 ) * (h" * (h |^ abs( j ))") by A2,Def8
        .= h |^ abs( j + 1 ) * ((h |^ abs( j ) * h)") by Th17
        .= h |^ abs( j + 1 ) * (h |^ (abs( j ) + 1))" by Lm6
        .= h |^ abs( j + 1 ) * (h |^ abs( j + 1 ))" by A3,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
      j < - 1;
      then
A4:   j + 1 < - 1 + 1 by XREAL_1:6;
      hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = (h |^ abs( j + 1 ))"
      * ((h |^ (-1)) * (h |^ (- j))) by Def8
        .= (h |^ abs( j + 1 ))" * (h" * (h |^ (- j))) by Th32
        .= (h |^ abs( j + 1 ))" * h" * (h |^ (- j)) by Def3
        .= (h * (h |^ abs( j + 1 )))" * (h |^ (- j)) by Th17
        .= (h |^ (abs( j + 1 ) + 1))" * (h |^ (- j)) by Lm6
        .= (h |^ (- (j + 1) + 1))" * (h |^ (- j)) by A4,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
A5:   j = - 1;
      hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = 1_G * ((h |^ (-1)) *
      (h |^ (- j))) by Lm3
        .= (h |^ (-1)) * (h |^ (- j)) by Def4
        .= h" * (h |^ (- j)) by Th32
        .= h" * (h |^ j)" by Lm12
        .= h" * h"" by A5,Th32
        .= 1_G by Def5;
    end;
  end;
  h |^ (j + 1) * (h |^ (- (j + 1))) = h |^ (j + 1) * (h |^ (j + 1))" by Lm12
    .= 1_G by Def5;
  then
A6: h |^ (- (j + 1)) = h |^ (-1) * (h |^ (- j)) by A1,Th6;
  thus h |^ (j + 1) = h |^ (- (- (j + 1)))
    .= ((h |^ (-1)) * (h |^ (- j)))" by A6,Lm12
    .= (h |^ (- j))" * (h |^ (-1))" by Th17
    .= h |^ (- (- j)) * (h |^ (-1))" by Lm12
    .= h |^ j * (h |^ (- (-1))) by Lm12
    .= h |^ j * (h |^ 1);
end;

theorem Th33:
  h |^ (i + j) = (h |^ i) * (h |^ j)
proof
  defpred P[Integer] means for i holds h |^ (i + $1) = h |^ i * (h |^ $1);
A1: for j holds P[j] implies P[j - 1] & P[j + 1]
  proof
    let j;
    assume
A2: for i holds h |^ (i + j) = h |^ i * (h |^ j);
    thus for i holds h |^ (i + (j - 1)) = h |^ i * (h |^ (j - 1))
    proof
      let i;
      thus h |^ (i + (j - 1)) = h |^ ((i - 1) + j)
        .= h |^ (i - 1) * (h |^ j) by A2
        .= h |^ i * (h |^ (-1)) * (h |^ j) by Lm14
        .= h |^ i * ((h |^ (-1)) * (h |^ j)) by Def3
        .= h |^ i * (h |^ (j + (-1))) by A2
        .= h |^ i * (h |^ (j - 1));
    end;
    let i;
    thus h |^ (i + (j + 1)) = h |^ ((i + 1) + j)
      .= h |^ (i + 1) * (h |^ j) by A2
      .= h |^ i * (h |^ 1) * (h |^ j) by Lm16
      .= h |^ i * ((h |^ 1) * (h |^ j)) by Def3
      .= h |^ i * (h |^ (j + 1)) by A2;
  end;
A3: P[0]
  proof
    let i;
    thus h |^ (i + 0) = h |^ i * 1_G by Def4
      .= h |^ i * (h |^ 0) by Def7;
  end;
  for j holds P[j] from INT_1:sch 4(A3,A1);
  hence thesis;
end;

theorem
  h |^ (i + 1) = h |^ i * h & h |^ (i + 1) = h * (h |^ i)
proof
  h |^ 1 = h by Th26;
  hence thesis by Th33;
end;

Lm17: h" |^ i = (h |^ i)"
proof
  per cases;
  suppose
    i >= 0;
    then reconsider n = i as Element of NAT by INT_1:3;
    thus h" |^ i = (h |^ n)" by Lm8
      .= (h |^ i)";
  end;
  suppose
A1: i < 0;
    hence h" |^ i = (h" |^ abs(i))" by Def8
      .= (h |^ abs(i))"" by Lm8
      .= (h |^ i)" by A1,Def8;
  end;
end;

theorem
  h |^ (i * j) = h |^ i |^ j
proof
  per cases;
  suppose
    i >= 0 & j >= 0;
    then reconsider m = i, n = j as Element of NAT by INT_1:3;
    thus h |^ (i * j) = h |^ m |^ n by Lm7
      .= h |^ i |^ j;
  end;
  suppose
    i >= 0 & j < 0;
    then reconsider m = i, n = - j as Element of NAT by INT_1:3;
    i * j = - (i * n);
    hence h |^ (i * j) = (h |^ (i * n))" by Lm12
      .= h" |^ (i * n) by Lm17
      .= h" |^ m |^ n by Lm7
      .= (h |^ i)" |^ n by Lm17
      .= ((h |^ i)" |^ j)" by Lm12
      .= (h |^ i |^ j)"" by Lm17
      .= h |^ i |^ j;
  end;
  suppose
    i < 0 & j >= 0;
    then reconsider m = - i, n = j as Element of NAT by INT_1:3;
    i * j = - (m * j);
    hence h |^ (i * j) = (h |^ (m * j))" by Lm12
      .= h" |^ (m * j) by Lm17
      .= h" |^ m |^ n by Lm7
      .= (h" |^ i)" |^ n by Lm12
      .= (h |^ i)"" |^ j by Lm17
      .= h |^ i |^ j;
  end;
  suppose
    j < 0 & i < 0;
    then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
    i * j * ((-1) * (-1)) = m * n;
    hence h |^ (i * j) = h |^ m |^ n by Lm7
      .= (h |^ (- i) |^ j)" by Lm12
      .= ((h |^ i)" |^ j)" by Lm12
      .= (h" |^ i |^ j)" by Lm17
      .= ((h" |^ i)") |^ j by Lm17
      .= h"" |^ i |^ j by Lm17
      .= h |^ i |^ j;
  end;
end;

theorem
  h |^ -i = (h |^ i)" by Lm12;

theorem
  h" |^ i = (h |^ i)" by Lm17;

theorem Th38:
  g * h = h * g implies (g * h) |^ i = g |^ i * (h |^ i)
proof
  assume
A1: g * h = h * g;
  per cases;
  suppose
A2: i >= 0;
    then
A3: h |^ i = h |^ abs(i) by Def8;
    (g * h) |^ i = (g * h) |^ abs(i) & g |^ i = g |^ abs(i) by A2,Def8;
    hence thesis by A1,A3,Lm11;
  end;
  suppose
A4: i < 0;
    hence (g * h) |^ i = ((h * g) |^ abs(i))" by A1,Def8
      .= (h |^ abs(i) * (g |^ abs(i)))" by A1,Lm11
      .= (g |^ abs(i))" * (h |^ abs(i))" by Th17
      .= g |^ i * (h |^ abs(i))" by A4,Def8
      .= g |^ i * (h |^ i) by A4,Def8;
  end;
end;

theorem Th39:
  g * h = h * g implies g |^ i * (h |^ j) = h |^ j * (g |^ i)
proof
  assume
A1: g * h = h * g;
  per cases;
  suppose
    i >= 0 & j >= 0;
    then g |^ i = g |^ abs(i) & h |^ j = h |^ abs( j ) by Def8;
    hence thesis by A1,Lm10;
  end;
  suppose
A2: i >= 0 & j < 0;
A3: g|^abs(i) * (h|^abs( j )) = h|^abs( j ) * (g|^abs(i)) by A1,Lm10;
    g |^ i = g |^ abs(i) & h |^ j = (h |^ abs( j ))" by A2,Def8;
    hence thesis by A3,Th20;
  end;
  suppose
A4: i < 0 & j >= 0;
A5: g|^abs(i) * (h|^abs( j )) = h|^abs( j ) * (g|^abs(i)) by A1,Lm10;
    g |^ i = (g |^ abs(i))" & h |^ j = h |^ abs( j ) by A4,Def8;
    hence thesis by A5,Th20;
  end;
  suppose
    i < 0 & j < 0;
    then
A6: g |^ i = (g |^ abs(i))" & h |^ j = (h |^ abs( j ))" by Def8;
    hence g |^ i * (h |^ j) = (h |^ abs( j ) * (g |^ abs(i)))" by Th17
      .= (g |^ abs(i) * (h |^ abs( j )))" by A1,Lm10
      .= h |^ j * (g |^ i) by A6,Th17;
  end;
end;

theorem
  g * h = h * g implies g * (h |^ i) = h |^ i * g
proof
  assume
A1: g * h = h * g;
  thus g * (h |^ i) = g |^ 1 * (h |^ i) by Th26
    .= h |^ i * (g |^ 1) by A1,Th39
    .= h |^ i * g by Th26;
end;

definition
  let G,h;
  attr h is being_of_order_0 means
  :Def10:
  h |^ n = 1_G implies n = 0;
end;

registration
  let G;
  cluster 1_G -> non being_of_order_0;
  coherence
  proof
    (1_G) |^ 8 = 1_G by Lm4;
    hence thesis by Def10;
  end;
end;

definition
  let G,h;
  func ord h -> Element of NAT means
  :Def11:
  it = 0 if h is being_of_order_0
  otherwise
  h |^ it = 1_G & it <> 0 & for m st h |^ m = 1_G & m <> 0 holds it <= m;
  existence
  proof
    defpred P[Nat] means h |^ $1 = 1_G & $1 <> 0;
    thus h is being_of_order_0 implies ex n being Element of NAT st n=0;
    hereby
      assume not h is being_of_order_0;
      then
A1:   ex n being Nat st P[n] by Def10;
      consider k being Nat such that
A2:   P[k] and
A3:   for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A1);
      reconsider k as Element of NAT by ORDINAL1:def 12;
      take k;
      thus h |^ k = 1_G & k <> 0 by A2;
      let m;
      assume h |^ m = 1_G & m <> 0;
      hence k <= m by A3;
    end;
  end;
  uniqueness
  proof
    let n1,n2 be Element of NAT;
    thus h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2;
    assume that
    not h is being_of_order_0 and
A4: h |^ n1 = 1_G & n1 <> 0 & ( for m st h |^ m = 1_G & m <> 0 holds
n1 <= m )& h |^ n2 = 1_G &( n2 <> 0 & for m st h |^ m = 1_G & m <> 0 holds n2
    <= m );
    n1 <= n2 & n2 <= n1 by A4;
    hence thesis by XXREAL_0:1;
  end;
  correctness;
end;

theorem Th41:
  h |^ ord h = 1_G
proof
  per cases;
  suppose
    h is being_of_order_0;
    then ord h = 0 by Def11;
    hence thesis by Def7;
  end;
  suppose
    h is not being_of_order_0;
    hence thesis by Def11;
  end;
end;

theorem
  ord 1_G = 1
proof
A1: for n st (1_G) |^ n = 1_G & n <> 0 holds 1 <= n by NAT_1:14;
  ( not 1_G is being_of_order_0)& (1_G) |^ 1 = 1_G by Lm4;
  hence thesis by A1,Def11;
end;

theorem
  ord h = 1 implies h = 1_G
proof
  assume
A1: ord h = 1;
  then not h is being_of_order_0 by Def11;
  then h |^ 1 = 1_G by A1,Def11;
  hence thesis by Th26;
end;

theorem
  h |^ n = 1_G implies ord h divides n
proof
  defpred P[Nat] means h |^ $1 = 1_G implies ord h divides $1;
A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
  proof
    let n be Nat;
    assume
A2: for k being Nat st k < n holds P[k];
    assume
A3: h |^ n = 1_G;
    per cases;
    suppose
      n = 0;
      hence thesis by NAT_D:6;
    end;
    suppose
A4:   n <> 0;
      per cases;
      suppose
        ord h = 0;
        then h is being_of_order_0 by Def11;
        hence thesis by A3,A4,Def10;
      end;
      suppose
A5:     ord h <> 0;
        then h is not being_of_order_0 by Def11;
        then ord h <= n by A3,A4,Def11;
        then consider m being Nat such that
A6:     n = ord h + m by NAT_1:10;
        h |^ n = h |^ ord h * (h |^ m) by A6,Lm5
          .= 1_G * (h |^ m) by Th41
          .= h |^ m by Def4;
        then ord h divides m by A2,A3,A5,A6,NAT_1:16;
        then consider i being Nat such that
A7:     m = ord h * i by NAT_D:def 3;
        n = ord h * (1 + i) by A6,A7;
        hence thesis by NAT_D:def 3;
      end;
    end;
  end;
  for n being Nat holds P[n] from NAT_1:sch 4(A1);
  hence thesis;
end;

definition
  let G be finite 1-sorted;

  redefine func card G -> Element of NAT;
  coherence
  proof
    card the carrier of G in NAT;
    hence thesis;
  end;
end;

theorem
  for G being non empty finite 1-sorted holds card G >= 1
proof
  let G be non empty finite 1-sorted;
  set g = the Element of G;
  {g} c= the carrier of G & card {g} = 1 by CARD_1:30,ZFMISC_1:31;
  hence thesis by NAT_1:43;
end;

definition

  let IT be multMagma;
  attr IT is commutative means
  :Def12:
  for x, y being Element of IT holds x*y = y*x;
end;

registration
  cluster strict commutative for Group;
  existence
  proof
    reconsider G0 = multMagma (# REAL, addreal #) as Group by Th3;
    take G0;
    thus G0 is strict;
    let a,g be Element of G0;
    reconsider A = a, B = g as Real;
    thus a * g = B + A by BINOP_2:def 9
      .= g * a by BINOP_2:def 9;
  end;
end;

definition
  let FS be commutative non empty multMagma;
  let x,y be Element of FS;
  redefine func x*y;
  commutativity by Def12;
end;

theorem
  multMagma (# REAL, addreal #) is commutative Group
proof
  reconsider G = multMagma (# REAL, addreal #) as Group by Th3;
  G is commutative
  proof
    let h,g be Element of G;
    reconsider A = h, B = g as Real;
    thus h * g = B + A by BINOP_2:def 9
      .= g * h by BINOP_2:def 9;
  end;
  hence thesis;
end;

reserve A for commutative Group;
reserve a,b for Element of A;

theorem
  (a * b)" = a" * b" by Th17;

theorem
  (a * b) |^ i = a |^ i * (b |^ i) by Th38;

theorem
  addLoopStr (# the carrier of A, the multF of A, 1_A #) is Abelian
  add-associative right_zeroed right_complementable
proof
  set G = addLoopStr (# the carrier of A, the multF of A, 1_A #);
  thus G is Abelian
  proof
    let a,b be Element of G;
    reconsider x = a, y = b as Element of A;
A1: for a,b be Element of G, x,y be Element of A st a = x & b = y holds a
    + b = x * y;
    thus a + b = x * y .= b + a by A1;
  end;
  hereby
    let a,b,c be Element of G;
    reconsider x = a, y = b, z = c as Element of A;
    thus a + b + c = x * y * z .= x * (y * z) by Def3
      .= a + (b + c);
  end;
  hereby
    let a be Element of G;
    reconsider x = a as Element of A;
    thus a + 0.G = x * 1_A .= a by Def4;
  end;
  let a be Element of G;
  reconsider x = a as Element of A;
  reconsider b = inverse_op(A).x as Element of G;
  take b;
  thus a + b = x * x" by Def6
    .= 0.G by Def5;
end;

begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.

theorem Th50:
  for L be unital non empty multMagma for x be Element of L holds
  (power L).(x,1) = x
proof
  let L be unital non empty multMagma;
  let x be Element of L;
  0+1 = 1;
  hence (power L).(x,1) = (power L).(x,0) * x by Def7
    .= 1_L * x by Def7
    .= x by Def4;
end;

theorem
  for L be unital non empty multMagma for x be Element of L holds (power
  L).(x,2) = x*x
proof
  let L be unital non empty multMagma;
  let x be Element of L;
  1+1 = 2;
  hence (power L).(x,2) = (power L).(x,1) * x by Def7
    .= x * x by Th50;
end;

theorem
  for L be associative commutative unital non empty multMagma for x,y be
Element of L for n be Element of NAT holds (power L).(x*y,n) = (power L).(x,n)
  * (power L).(y,n)
proof
  let L be associative commutative unital non empty multMagma;
  let x,y be Element of L;
  defpred P[Element of NAT] means (power L).(x*y,$1) = (power L).(x,$1) * (
  power L).(y,$1);
A1: now
    let n be Element of NAT;
    assume P[n];
    then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by
Def7
      .= (power L).(x,n) * ((power L).(y,n) * (x*y)) by Def3
      .= (power L).(x,n) * (x*((power L).(y,n)*y)) by Def3
      .= (power L).(x,n) * (x*(power L).(y,n+1)) by Def7
      .= (power L).(x,n)*x * (power L).(y,n+1) by Def3
      .= (power L).(x,n+1) * (power L).(y,n+1) by Def7;
    hence P[n+1];
  end;
  (power L).(x*y,0) = 1_L by Def7
    .= 1_L * 1_L by Def4
    .= (power L).(x,0) * 1_L by Def7
    .= (power L).(x,0) * (power L).(y,0) by Def7;
  then
A2: P[0];
  thus for n be Element of NAT holds P[n] from NAT_1:sch 1(A2,A1);
end;
 
:: Moved from ENDALG, 17.01_2006, AK

definition
  let G,H be multMagma;
  let IT be Function of G,H;
  attr IT is unity-preserving means
  IT.1_G = 1_H;
end;