:: GROUP_1 semantic presentation

begin


Lm1: now__::_thesis:_(_(_for_h,_g,_f_being_Element_of_multMagma(#_REAL,addreal_#)_holds_(h_*_g)_*_f_=_h_*_(g_*_f)_)_&_ex_e_being_Element_of_multMagma(#_REAL,addreal_#)_st_
for_h_being_Element_of_multMagma(#_REAL,addreal_#)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_&_ex_g_being_Element_of_multMagma(#_REAL,addreal_#)_st_
(_h_*_g_=_e_&_g_*_h_=_e_)_)_)
set G = multMagma(# REAL,addreal #);
thus  for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) ::_thesis: ex e being Element of multMagma(# REAL,addreal #) st
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
proof
let h, g, f be Element of multMagma(# REAL,addreal #); ::_thesis: (h * g) * f = h * (g * f)
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 ;
::_thesis: verum
end;
reconsider e = 0 as Element of multMagma(# REAL,addreal #) ;
take e = e; ::_thesis: for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# REAL,addreal #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
reconsider A = h as Real ;
thus h * e = A + 0 by BINOP_2:def_9
.= h ; ::_thesis: ( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
thus e * h = 0 + A by BINOP_2:def_9
.= h ; ::_thesis: ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e )
reconsider g = - A as Element of multMagma(# REAL,addreal #) ;
take g = g; ::_thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by BINOP_2:def_9
.= e ; ::_thesis: g * h = e
thus g * h = (- A) + A by BINOP_2:def_9
.= e ; ::_thesis: verum
end;

definition
let IT be multMagma ;
attrIT is unital  means :Def1: :: GROUP_1:def 1
 ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h );
attrIT is Group-like  means :Def2: :: GROUP_1:def 2
 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 ) );
attrIT is associative  means :Def3: :: GROUP_1:def 3
 for x, y, z being Element of IT holds (x * y) * z = x * (y * z);
end;

:: deftheorem Def1 defines unital GROUP_1:def_1_:_
 for IT being multMagma holds
( IT is unital iff ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) );

:: deftheorem Def2 defines Group-like GROUP_1:def_2_:_
 for IT being multMagma holds
( IT is Group-like iff 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 ) ) );

:: deftheorem Def3 defines associative GROUP_1:def_3_:_
 for IT being multMagma holds
( IT is associative iff for x, y, z being Element of IT holds (x * y) * z = x * (y * z) );

registration
cluster Group-like  ->  unital for multMagma ;
coherence
 for b1 being multMagma st b1 is Group-like holds
b1 is unital
proof
let IT be multMagma ; ::_thesis: ( IT is Group-like implies IT is unital )
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 ) ) ; :: according to GROUP_1:def_2 ::_thesis: IT is unital
hence  ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) ; :: according to GROUP_1:def_1 ::_thesis: verum
end;
end;

registration
cluster non empty strict Group-like associative for multMagma ;
existence
 ex b1 being multMagma st
( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty )
proof
 ( multMagma(# REAL,addreal #) is Group-like & multMagma(# REAL,addreal #) is associative ) by Def2, Def3, Lm1;
hence  ex b1 being multMagma st
( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty ) ; ::_thesis: verum
end;
end;

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

theorem :: GROUP_1:1
for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ex t being Element of S st
for s1 being Element of S holds
( s1 * t = s1 & t * s1 = s1 & ex s2 being Element of S st
( s1 * s2 = t & s2 * s1 = t ) ) holds
S is Group by Def2, Def3;

theorem :: GROUP_1:2
for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) holds
( S is associative & S is Group-like )
proof
let S be non empty multMagma ; ::_thesis: ( ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) implies ( S is associative & S is Group-like ) )
set r = the Element of S;
assume that
A1: for r, s, t being Element of S holds (r * s) * t = r * (s * t) and
A2: for r, s being Element of S holds
( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ; ::_thesis: ( S is associative & S is Group-like )
consider s1 being Element of S such that
A3: the Element of S * s1 = the Element of S by A2;
thus  for r, s, t being Element of S holds (r * s) * t = r * (s * t) by A1; :: according to GROUP_1:def_3 ::_thesis: S is Group-like
take  s1 ; :: according to GROUP_1:def_2 ::_thesis: for h being Element of S holds
( h * s1 = h & s1 * h = h & ex g being Element of S st
( h * g = s1 & g * h = s1 ) )
let s be Element of S; ::_thesis: ( s * s1 = s & s1 * s = s & ex g being Element of S st
( s * g = s1 & g * s = s1 ) )
 ex t being Element of S st t * the Element of S = s by A2;
hence A4: s * s1 = s by A1, A3; ::_thesis: ( s1 * s = s & ex g being Element of S st
( s * g = s1 & g * s = s1 ) )
consider s2 being Element of S such that
A5: s2 * the Element of S = the Element of S by A2;
consider t1 being Element of S such that
A6: the Element of S * t1 = s1 by A2;
A7: ex t2 being Element of S st t2 * the Element of S = s2 by A2;
A8: s1 = s2 * ( the Element of S * t1) by A1, A5, A6
.= s2 by A1, A3, A6, A7 ;
 ex t being Element of S st the Element of S * t = s by A2;
hence A9: s1 * s = s by A1, A5, A8; ::_thesis: ex g being Element of S st
( s * g = s1 & g * s = s1 )
consider t1 being Element of S such that
A10: s * t1 = s1 by A2;
consider t2 being Element of S such that
A11: t2 * s = s1 by A2;
take  t1 ; ::_thesis: ( s * t1 = s1 & t1 * s = s1 )
consider r1 being Element of S such that
A12: s * r1 = t1 by A2;
A13: ex r2 being Element of S 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  ( s * t1 = s1 & t1 * s = s1 ) by A10, A11; ::_thesis: verum
end;

theorem Th3: :: GROUP_1:3
( multMagma(# REAL,addreal #) is associative & multMagma(# REAL,addreal #) is Group-like )
proof
set G = multMagma(# REAL,addreal #);
thus  for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def_3 ::_thesis: multMagma(# REAL,addreal #) is Group-like
proof
let h, g, f be Element of multMagma(# REAL,addreal #); ::_thesis: (h * g) * f = h * (g * f)
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 ;
::_thesis: verum
end;
reconsider e = 0 as Element of multMagma(# REAL,addreal #) ;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# REAL,addreal #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
reconsider A = h as Real ;
thus h * e = A + 0 by BINOP_2:def_9
.= h ; ::_thesis: ( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
thus e * h = 0 + A by BINOP_2:def_9
.= h ; ::_thesis: ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e )
reconsider g = - A as Element of multMagma(# REAL,addreal #) ;
take  g ; ::_thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by BINOP_2:def_9
.= e ; ::_thesis: g * h = e
thus g * h = (- A) + A by BINOP_2:def_9
.= e ; ::_thesis: verum
end;


definition
let G be multMagma ;
assume A1: G is unital ;
func 1_ G ->  Element of G means :Def4: :: GROUP_1:def 4
 for h being Element of G holds
( h * it = h & it * h = h );
existence
 ex b1 being Element of G st
for h being Element of G holds
( h * b1 = h & b1 * h = h ) by A1, Def1;
uniqueness
 for b1, b2 being Element of G st ( for h being Element of G holds
( h * b1 = h & b1 * h = h ) ) & ( for h being Element of G holds
( h * b2 = h & b2 * h = h ) ) holds
b1 = b2
proof
let e1, e2 be Element of G; ::_thesis: ( ( for h being Element of G holds
( h * e1 = h & e1 * h = h ) ) & ( for h being Element of G holds
( h * e2 = h & e2 * h = h ) ) implies e1 = e2 )
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 ) ; ::_thesis: e1 = e2
thus e1 = e2 * e1 by A2
.= e2 by A1 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines 1_ GROUP_1:def_4_:_
 for G being multMagma st G is unital holds
for b2 being Element of G holds
( b2 = 1_ G iff for h being Element of G holds
( h * b2 = h & b2 * h = h ) );

theorem :: GROUP_1:4
for G being non empty Group-like multMagma
for e being Element of G st ( for h being Element of G holds
( h * e = h & e * h = h ) ) holds
e = 1_ G by Def4;


definition
let G be Group;
let h be Element of G;
funch "  ->  Element of G means :Def5: :: GROUP_1:def 5
( h * it = 1_ G & it * h = 1_ G );
existence
 ex b1 being Element of G st
( h * b1 = 1_ G & b1 * h = 1_ G )
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 ; ::_thesis: ( h * g = 1_ G & g * h = 1_ G )
thus  ( h * g = 1_ G & g * h = 1_ G ) by A1, A2, Def4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of G st h * b1 = 1_ G & b1 * h = 1_ G & h * b2 = 1_ G & b2 * h = 1_ G holds
b1 = b2
proof
let h1, h2 be Element of G; ::_thesis: ( h * h1 = 1_ G & h1 * h = 1_ G & h * h2 = 1_ G & h2 * h = 1_ G implies h1 = h2 )
assume that
A3: h * h1 = 1_ G and
 h1 * h = 1_ G and
 h * h2 = 1_ G and
A4: h2 * h = 1_ G ; ::_thesis: h1 = h2
thus h1 = (1_ G) * h1 by Def4
.= h2 * (h * h1) by A4, Def3
.= h2 by A3, Def4 ; ::_thesis: verum
end;
involutiveness
 for b1, b2 being Element of G st b2 * b1 = 1_ G & b1 * b2 = 1_ G holds
( b1 * b2 = 1_ G & b2 * b1 = 1_ G ) ;
end;

:: deftheorem Def5 defines " GROUP_1:def_5_:_
 for G being Group
for h, b3 being Element of G holds
( b3 = h " iff ( h * b3 = 1_ G & b3 * h = 1_ G ) );

theorem :: GROUP_1:5
for G being Group
for h, g being Element of G st h * g = 1_ G & g * h = 1_ G holds
g = h " by Def5;

theorem Th6: :: GROUP_1:6
for G being Group
for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f
proof
let G be Group; ::_thesis: for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f
let h, g, f be Element of G; ::_thesis: ( ( h * g = h * f or g * h = f * h ) implies g = f )
assume  ( h * g = h * f or g * h = f * h ) ; ::_thesis: g = f
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  g = f by Def4; ::_thesis: verum
end;

theorem :: GROUP_1:7
for G being Group
for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
proof
let G be Group; ::_thesis: for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
let h, g be Element of G; ::_thesis: ( ( h * g = h or g * h = h ) implies g = 1_ G )
 ( h * (1_ G) = h & (1_ G) * h = h ) by Def4;
hence  ( ( h * g = h or g * h = h ) implies g = 1_ G ) by Th6; ::_thesis: verum
end;

theorem Th8: :: GROUP_1:8
for G being Group holds (1_ G) " = 1_ G
proof
let G be Group; ::_thesis: (1_ G) " = 1_ G
 ((1_ G) ") * (1_ G) = 1_ G by Def5;
hence  (1_ G) " = 1_ G by Def4; ::_thesis: verum
end;

theorem :: GROUP_1:9
for G being Group
for h, g being Element of G st h " = g " holds
h = g
proof
let G be Group; ::_thesis: for h, g being Element of G st h " = g " holds
h = g
let h, g be Element of G; ::_thesis: ( h " = g " implies h = g )
assume  h " = g " ; ::_thesis: h = g
then A1: h * (g ") = 1_ G by Def5;
 g * (g ") = 1_ G by Def5;
hence  h = g by A1, Th6; ::_thesis: verum
end;

theorem :: GROUP_1:10
for G being Group
for h being Element of G st h " = 1_ G holds
h = 1_ G
proof
let G be Group; ::_thesis: for h being Element of G st h " = 1_ G holds
h = 1_ G
let h be Element of G; ::_thesis: ( h " = 1_ G implies h = 1_ G )
 (1_ G) " = 1_ G by Th8;
hence  ( h " = 1_ G implies h = 1_ G ) ; ::_thesis: verum
end;

theorem :: GROUP_1:11
canceled;

theorem Th12: :: GROUP_1:12
for G being Group
for h, g being Element of G st h * g = 1_ G holds
( h = g " & g = h " )
proof
let G be Group; ::_thesis: for h, g being Element of G st h * g = 1_ G holds
( h = g " & g = h " )
let h, g be Element of G; ::_thesis: ( h * g = 1_ G implies ( h = g " & g = h " ) )
assume A1: h * g = 1_ G ; ::_thesis: ( h = g " & g = h " )
 ( h * (h ") = 1_ G & (g ") * g = 1_ G ) by Def5;
hence  ( h = g " & g = h " ) by A1, Th6; ::_thesis: verum
end;

theorem Th13: :: GROUP_1:13
for G being Group
for h, f, g being Element of G holds
( h * f = g iff f = (h ") * g )
proof
let G be Group; ::_thesis: for h, f, g being Element of G holds
( h * f = g iff f = (h ") * g )
let h, f, g be Element of G; ::_thesis: ( h * f = g iff f = (h ") * g )
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; ::_thesis: ( f = (h ") * g implies h * f = g )
assume  f = (h ") * g ; ::_thesis: h * f = g
hence h * f = (h * (h ")) * g by Def3
.= (1_ G) * g by Def5
.= g by Def4 ;
::_thesis: verum
end;

theorem Th14: :: GROUP_1:14
for G being Group
for f, h, g being Element of G holds
( f * h = g iff f = g * (h ") )
proof
let G be Group; ::_thesis: for f, h, g being Element of G holds
( f * h = g iff f = g * (h ") )
let f, h, g be Element of G; ::_thesis: ( f * h = g iff f = g * (h ") )
(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; ::_thesis: ( f = g * (h ") implies f * h = g )
assume  f = g * (h ") ; ::_thesis: f * h = g
hence f * h = g * ((h ") * h) by Def3
.= g * (1_ G) by Def5
.= g by Def4 ;
::_thesis: verum
end;

theorem :: GROUP_1:15
for G being Group
for g, h being Element of G ex f being Element of G st g * f = h
proof
let G be Group; ::_thesis: for g, h being Element of G ex f being Element of G st g * f = h
let g, h be Element of G; ::_thesis: ex f being Element of G st g * f = h
take  (g ") * h ; ::_thesis: g * ((g ") * h) = h
thus  g * ((g ") * h) = h by Th13; ::_thesis: verum
end;

theorem :: GROUP_1:16
for G being Group
for g, h being Element of G ex f being Element of G st f * g = h
proof
let G be Group; ::_thesis: for g, h being Element of G ex f being Element of G st f * g = h
let g, h be Element of G; ::_thesis: ex f being Element of G st f * g = h
take  h * (g ") ; ::_thesis: (h * (g ")) * g = h
thus  (h * (g ")) * g = h by Th14; ::_thesis: verum
end;

theorem Th17: :: GROUP_1:17
for G being Group
for h, g being Element of G holds (h * g) " = (g ") * (h ")
proof
let G be Group; ::_thesis: for h, g being Element of G holds (h * g) " = (g ") * (h ")
let h, g be Element of G; ::_thesis: (h * g) " = (g ") * (h ")
((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  (h * g) " = (g ") * (h ") by Th12; ::_thesis: verum
end;

theorem Th18: :: GROUP_1:18
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
proof
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff (g * h) " = (g ") * (h ") )
thus  ( g * h = h * g implies (g * h) " = (g ") * (h ") ) by Th17; ::_thesis: ( (g * h) " = (g ") * (h ") implies g * h = h * g )
assume  (g * h) " = (g ") * (h ") ; ::_thesis: g * h = h * g
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  g * h = h * g by A1, Th6; ::_thesis: verum
end;

theorem Th19: :: GROUP_1:19
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
proof
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
thus  ( g * h = h * g implies (g ") * (h ") = (h ") * (g ") ) ::_thesis: ( (g ") * (h ") = (h ") * (g ") implies g * h = h * g )
proof
assume A1: g * h = h * g ; ::_thesis: (g ") * (h ") = (h ") * (g ")
hence (g ") * (h ") = (g * h) " by Th17
.= (h ") * (g ") by A1, Th18 ;
::_thesis: verum
end;
assume A2: (g ") * (h ") = (h ") * (g ") ; ::_thesis: g * h = h * g
thus g * h = ((g * h) ") "
.= ((h ") * (g ")) " by Th17
.= ((h ") ") * ((g ") ") by A2, Th17
.= h * g ; ::_thesis: verum
end;

theorem Th20: :: GROUP_1:20
for G being Group
for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
proof
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff g * (h ") = (h ") * g )
thus  ( g * h = h * g implies g * (h ") = (h ") * g ) ::_thesis: ( g * (h ") = (h ") * g implies g * h = h * g )
proof
assume A1: g * h = h * g ; ::_thesis: 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  g * (h ") = (h ") * g ; ::_thesis: verum
end;
assume  g * (h ") = (h ") * g ; ::_thesis: 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  g * h = h * g by Def4; ::_thesis: verum
end;

definition
let G be Group;
func inverse_op G ->  UnOp of G means :Def6: :: GROUP_1:def 6
 for h being Element of G holds it . h = h " ;
existence
 ex b1 being UnOp of G st
for h being Element of G holds b1 . h = h "
proof
deffunc H1( Element of G) ->  Element of G = $1 " ;
consider u being UnOp of G such that
A1: for h being Element of G holds u . h = H1(h) from FUNCT_2:sch_4();
take  u ; ::_thesis: for h being Element of G holds u . h = h "
let h be Element of G; ::_thesis: u . h = h "
thus  u . h = h " by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of G st ( for h being Element of G holds b1 . h = h " ) & ( for h being Element of G holds b2 . h = h " ) holds
b1 = b2
proof
let u1, u2 be UnOp of G; ::_thesis: ( ( for h being Element of G holds u1 . h = h " ) & ( for h being Element of G holds u2 . h = h " ) implies u1 = u2 )
assume A2: for h being Element of G holds u1 . h = h " ; ::_thesis: ( ex h being Element of G st not u2 . h = h " or u1 = u2 )
assume A3: for h being Element of G holds u2 . h = h " ; ::_thesis: u1 = u2
let h be Element of G; :: according to FUNCT_2:def_8 ::_thesis: u1 . h = u2 . h
thus u1 . h = h " by A2
.= u2 . h by A3 ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines inverse_op GROUP_1:def_6_:_
 for G being Group
for b2 being UnOp of G holds
( b2 = inverse_op G iff for h being Element of G holds b2 . h = h " );

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

theorem Th21: :: GROUP_1:21
for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G
proof
let G be non empty unital multMagma ; ::_thesis: 1_ G is_a_unity_wrt the multF of G
set o = the multF of G;
now__::_thesis:_for_h_being_Element_of_G_holds_
(_the_multF_of_G_._((1__G),h)_=_h_&_the_multF_of_G_._(h,(1__G))_=_h_)
let h be Element of G; ::_thesis: ( the multF of G . ((1_ G),h) = h & the multF of G . (h,(1_ G)) = h )
thus  the multF of G . ((1_ G),h) = (1_ G) * h
.= h by Def4 ; ::_thesis: the multF of G . (h,(1_ G)) = h
thus  the multF of G . (h,(1_ G)) = h * (1_ G)
.= h by Def4 ; ::_thesis: verum
end;
hence  1_ G is_a_unity_wrt the multF of G by BINOP_1:3; ::_thesis: verum
end;

theorem Th22: :: GROUP_1:22
for G being non empty unital multMagma holds the_unity_wrt the multF of G = 1_ G
proof
let G be non empty unital multMagma ; ::_thesis: the_unity_wrt the multF of G = 1_ G
 1_ G is_a_unity_wrt the multF of G by Th21;
hence  the_unity_wrt the multF of G = 1_ G by BINOP_1:def_8; ::_thesis: verum
end;

registration
let G be non empty unital multMagma ;
cluster the multF of G ->  having_a_unity ;
coherence
 the multF of G is having_a_unity
proof
take  1_ G ; :: according to SETWISEO:def_2 ::_thesis: 1_ G is_a_unity_wrt the multF of G
thus  1_ G is_a_unity_wrt the multF of G by Th21; ::_thesis: verum
end;
end;

theorem Th23: :: GROUP_1:23
for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G
proof
let G be Group; ::_thesis: inverse_op G is_an_inverseOp_wrt the multF of G
let h be Element of G; :: according to FINSEQOP:def_1 ::_thesis: ( the multF of G . (h,((inverse_op G) . h)) = the_unity_wrt the multF of G & the multF of G . (((inverse_op G) . h),h) = the_unity_wrt the multF 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 ; ::_thesis: the multF of G . (((inverse_op G) . h),h) = the_unity_wrt the multF of G
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 ; ::_thesis: verum
end;

registration
let G be Group;
cluster the multF of G ->  having_an_inverseOp ;
coherence
 the multF of G is having_an_inverseOp
proof
 inverse_op G is_an_inverseOp_wrt the multF of G by Th23;
hence  the multF of G is having_an_inverseOp by FINSEQOP:def_2; ::_thesis: verum
end;
end;

theorem :: GROUP_1:24
for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G
proof
let G be Group; ::_thesis: the_inverseOp_wrt the multF of G = inverse_op G
set o = the multF of G;
 ( the multF of G is having_an_inverseOp & inverse_op G is_an_inverseOp_wrt the multF of G ) by Th23;
hence  the_inverseOp_wrt the multF of G = inverse_op G by FINSEQOP:def_3; ::_thesis: verum
end;

definition
let G be non empty multMagma ;
func power G ->  Function of [: the carrier of G,NAT:], the carrier of G means :Def7: :: GROUP_1:def 7
 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
 ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st
for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) )
proof
defpred S1[ set , set ] means  ex g0 being Function of NAT, the carrier of G ex h being Element of G st
( $1 = h & g0 = $2 & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) );
A1: for x being set st x in the carrier of G holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of G implies ex y being set st S1[x,y] )
assume  x in the carrier of G ; ::_thesis: ex y being set st S1[x,y]
then reconsider b = x as Element of G ;
deffunc H1( Nat, Element of G) ->  Element of the carrier 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) = H1(n,g0 . n) from NAT_1:sch_12();
reconsider y = g0 as set ;
take  y ; ::_thesis: S1[x,y]
take  g0 ; ::_thesis: ex h being Element of G st
( x = h & g0 = y & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) )
take  b ; ::_thesis: ( x = b & g0 = y & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * b ) )
thus  ( x = b & g0 = y & g0 . 0 = 1_ G ) by A2; ::_thesis: for n being Nat holds g0 . (n + 1) = (g0 . n) * b
let n be Nat; ::_thesis: g0 . (n + 1) = (g0 . n) * b
thus  g0 . (n + 1) = (g0 . n) * b by A3; ::_thesis: verum
end;
consider f being Function such that
 dom f = the carrier of G and
A4: for x being set st x in the carrier of G holds
S1[x,f . x] from CLASSES1:sch_1(A1);
defpred S2[ 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
for n being Element of NAT ex b being Element of G st S2[a,n,b]
proof
let a be Element of G; ::_thesis: for n being Element of NAT ex b being Element of G st S2[a,n,b]
let n be Element of NAT ; ::_thesis: ex b being Element of G st S2[a,n,b]
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 being Nat holds g0 . (n + 1) = (g0 . n) * h by A4;
take  g0 . n ; ::_thesis: S2[a,n,g0 . n]
take  g0 ; ::_thesis: ( g0 = f . a & g0 . n = g0 . n )
thus  ( g0 = f . a & g0 . n = g0 . n ) by A6; ::_thesis: verum
end;
consider F being Function of [: the carrier of G,NAT:], the carrier of G such that
A7: for a being Element of G
for n being Element of NAT holds S2[a,n,F . (a,n)] from BINOP_1:sch_3(A5);
take  F ; ::_thesis: 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 ) )
let h be Element of G; ::_thesis: ( F . (h,0) = 1_ G & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
A8: ex g2 being Function of NAT, the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 1_ G & ( for n being Nat 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; ::_thesis: for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h
let n be Element of NAT ; ::_thesis: F . (h,(n + 1)) = (F . (h,n)) * h
A9: ex g2 being Function of NAT, the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 1_ G & ( for n being Nat 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  F . (h,(n + 1)) = (F . (h,n)) * h by A9; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of G holds
( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of G,NAT:], the carrier of G; ::_thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies f = 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 ) ) ; ::_thesis: f = g
now__::_thesis:_for_h_being_Element_of_G
for_n_being_Element_of_NAT_holds_f_._(h,n)_=_g_._(h,n)
let h be Element of G; ::_thesis: for n being Element of NAT holds f . (h,n) = g . (h,n)
let n be Element of NAT ; ::_thesis: f . (h,n) = g . (h,n)
defpred S1[ Nat] means f . [h,$1] = g . [h,$1];
A12: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A13: S1[n] ; ::_thesis: S1[n + 1]
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  S1[n + 1] ; ::_thesis: verum
end;
f . [h,0] = f . (h,0)
.= 1_ G by A10
.= g . (h,0) by A11
.= g . [h,0] ;
then A15: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A12);
hence  f . (h,n) = g . (h,n) ; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines power GROUP_1:def_7_:_
 for G being non empty multMagma
for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds
( b2 = power G iff for h being Element of G holds
( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) );

definition
let G be Group;
let i be Integer;
let h be Element of G;
funch |^ i ->  Element of G equals :Def8: :: GROUP_1:def 8
(power G) . (h,(abs i)) if  0 <= i
otherwise ((power G) . (h,(abs i))) " ;
correctness
coherence
( ( 0 <= i implies (power G) . (h,(abs i)) is Element of G ) & ( not 0 <= i implies ((power G) . (h,(abs i))) " is Element of G ) );
consistency
for b1 being Element of G holds verum;
;
end;

:: deftheorem Def8 defines |^ GROUP_1:def_8_:_
 for G being Group
for i being Integer
for h being Element of G holds
( ( 0 <= i implies h |^ i = (power G) . (h,(abs i)) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,(abs i))) " ) );

definition
let G be Group;
let n be Nat;
let h be Element of G;
redefine func h |^ n equals :: GROUP_1:def 9
(power G) . (h,n);
compatibility
 for b1 being Element of G holds
( b1 = h |^ n iff b1 = (power G) . (h,n) )
proof
let g be Element of G; ::_thesis: ( g = h |^ n iff g = (power G) . (h,n) )
 abs n = n by ABSVALUE:def_1;
hence  ( g = h |^ n iff g = (power G) . (h,n) ) by Def8; ::_thesis: verum
end;
end;

:: deftheorem  defines |^ GROUP_1:def_9_:_
 for G being Group
for n being Nat
for h being Element of G holds h |^ n = (power G) . (h,n);

Lm2:  for n being Nat
for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
proof
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let G be Group; ::_thesis: for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let h be Element of G; ::_thesis: h |^ (n + 1) = (h |^ n) * h
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 h |^ (n + 1) = (h |^ n) * h by Def7;
hence  h |^ (n + 1) = (h |^ n) * h ; ::_thesis: verum
end;

Lm3:  for G being Group
for h being Element of G holds h |^ 0 = 1_ G
by Def7;

Lm4:  for n being Nat
for G being Group holds (1_ G) |^ n = 1_ G
proof
let n be Nat; ::_thesis: for G being Group holds (1_ G) |^ n = 1_ G
let G be Group; ::_thesis: (1_ G) |^ n = 1_ G
defpred S1[ Nat] means (1_ G) |^ $1 = 1_ G;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then (1_ G) |^ (n + 1) = (1_ G) * (1_ G) by Lm2
.= 1_ G by Def4 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by Def7;
 for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1);
hence  (1_ G) |^ n = 1_ G ; ::_thesis: verum
end;

theorem :: GROUP_1:25
for G being Group
for h being Element of G holds h |^ 0 = 1_ G by Def7;

theorem Th26: :: GROUP_1:26
for G being Group
for h being Element of G holds h |^ 1 = h
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ 1 = h
let h be Element of G; ::_thesis: h |^ 1 = h
thus h |^ 1 = h |^ (0 + 1)
.= (h |^ 0) * h by Lm2
.= (1_ G) * h by Def7
.= h by Def4 ; ::_thesis: verum
end;

theorem Th27: :: GROUP_1:27
for G being Group
for h being Element of G holds h |^ 2 = h * h
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ 2 = h * h
let h be Element of G; ::_thesis: h |^ 2 = h * h
thus h |^ 2 = h |^ (1 + 1)
.= (h |^ 1) * h by Lm2
.= h * h by Th26 ; ::_thesis: verum
end;

theorem :: GROUP_1:28
for G being Group
for h being Element of G holds h |^ 3 = (h * h) * h
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ 3 = (h * h) * h
let h be Element of G; ::_thesis: h |^ 3 = (h * h) * h
thus h |^ 3 = h |^ (2 + 1)
.= (h |^ 2) * h by Lm2
.= (h * h) * h by Th27 ; ::_thesis: verum
end;

theorem :: GROUP_1:29
for G being Group
for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
proof
let G be Group; ::_thesis: for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
let h be Element of G; ::_thesis: ( h |^ 2 = 1_ G iff h " = h )
thus  ( h |^ 2 = 1_ G implies h = h " ) ::_thesis: ( h " = h implies h |^ 2 = 1_ G )
proof
assume  h |^ 2 = 1_ G ; ::_thesis: h = h "
then  h * h = 1_ G by Th27;
hence  h = h " by Th12; ::_thesis: verum
end;
assume  h = h " ; ::_thesis: h |^ 2 = 1_ G
hence h |^ 2 = h * (h ") by Th27
.= 1_ G by Def5 ;
::_thesis: verum
end;

Lm5:  for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
proof
let n, m be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let G be Group; ::_thesis: for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let h be Element of G; ::_thesis: h |^ (n + m) = (h |^ n) * (h |^ m)
defpred S1[ Nat] means  for n being Nat holds h |^ (n + $1) = (h |^ n) * (h |^ $1);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: for n being Nat holds h |^ (n + m) = (h |^ n) * (h |^ m) ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: h |^ (n + (m + 1)) = (h |^ n) * (h |^ (m + 1))
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 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let n be Nat; ::_thesis: h |^ (n + 0) = (h |^ n) * (h |^ 0)
thus h |^ (n + 0) = (h |^ n) * (1_ G) by Def4
.= (h |^ n) * (h |^ 0) by Def7 ; ::_thesis: verum
end;
 for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1);
hence  h |^ (n + m) = (h |^ n) * (h |^ m) ; ::_thesis: verum
end;

Lm6:  for n being Nat
for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
proof
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let G be Group; ::_thesis: for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let h be Element of G; ::_thesis: ( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
thus  h |^ (n + 1) = (h |^ n) * h by Lm2; ::_thesis: h |^ (n + 1) = h * (h |^ n)
thus h |^ (n + 1) = (h |^ 1) * (h |^ n) by Lm5
.= h * (h |^ n) by Th26 ; ::_thesis: verum
end;

Lm7:  for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
proof
let n, m be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let G be Group; ::_thesis: for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let h be Element of G; ::_thesis: h |^ (n * m) = (h |^ n) |^ m
defpred S1[ Nat] means  for n being Nat holds h |^ (n * $1) = (h |^ n) |^ $1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: for n being Nat holds h |^ (n * m) = (h |^ n) |^ m ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: h |^ (n * (m + 1)) = (h |^ n) |^ (m + 1)
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 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let n be Nat; ::_thesis: h |^ (n * 0) = (h |^ n) |^ 0
thus h |^ (n * 0) = 1_ G by Def7
.= (h |^ n) |^ 0 by Def7 ; ::_thesis: verum
end;
 for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1);
hence  h |^ (n * m) = (h |^ n) |^ m ; ::_thesis: verum
end;

Lm8:  for n being Nat
for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
proof
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
let G be Group; ::_thesis: for h being Element of G holds (h ") |^ n = (h |^ n) "
let h be Element of G; ::_thesis: (h ") |^ n = (h |^ n) "
defpred S1[ Nat] means (h ") |^ $1 = (h |^ $1) " ;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then (h ") |^ (n + 1) = ((h |^ n) ") * (h ") by Lm2
.= (h * (h |^ n)) " by Th17
.= (h |^ (n + 1)) " by Lm6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(h ") |^ 0 = 1_ G by Def7
.= (1_ G) " by Th8
.= (h |^ 0) " by Def7 ;
then A2: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1);
hence  (h ") |^ n = (h |^ n) " ; ::_thesis: verum
end;

Lm9:  for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
proof
let n be Nat; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
let g, h be Element of G; ::_thesis: ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g )
defpred S1[ Nat] means ( g * h = h * g implies g * (h |^ $1) = (h |^ $1) * g );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g ) ; ::_thesis: S1[n + 1]
assume A3: g * h = h * g ; ::_thesis: g * (h |^ (n + 1)) = (h |^ (n + 1)) * 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 ; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
assume  g * h = h * g ; ::_thesis: g * (h |^ 0) = (h |^ 0) * g
thus g * (h |^ 0) = g * (1_ G) by Def7
.= g by Def4
.= (1_ G) * g by Def4
.= (h |^ 0) * g by Def7 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence  ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g ) ; ::_thesis: verum
end;

Lm10:  for n, m being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
proof
let n, m be Nat; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) )
defpred S1[ Nat] means  for m being Nat st g * h = h * g holds
(g |^ $1) * (h |^ m) = (h |^ m) * (g |^ $1);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for m being Nat st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ; ::_thesis: S1[n + 1]
let m be Nat; ::_thesis: ( g * h = h * g implies (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1)) )
assume A3: g * h = h * g ; ::_thesis: (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1))
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 ; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
let m be Nat; ::_thesis: ( g * h = h * g implies (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0) )
assume  g * h = h * g ; ::_thesis: (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0)
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 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence  ( g * h = h * g implies (g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ) ; ::_thesis: verum
end;

Lm11:  for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
proof
let n be Nat; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) )
defpred S1[ Nat] means ( g * h = h * g implies (g * h) |^ $1 = (g |^ $1) * (h |^ $1) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) ) ; ::_thesis: S1[n + 1]
assume A3: g * h = h * g ; ::_thesis: (g * h) |^ (n + 1) = (g |^ (n + 1)) * (h |^ (n + 1))
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 ;
::_thesis: verum
end;
A4: S1[ 0 ]
proof
assume  g * h = h * g ; ::_thesis: (g * h) |^ 0 = (g |^ 0) * (h |^ 0)
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 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence  ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) ) ; ::_thesis: verum
end;

theorem Th30: :: GROUP_1:30
for i being Integer
for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let G be Group; ::_thesis: for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let h be Element of G; ::_thesis: ( i <= 0 implies h |^ i = (h |^ (abs i)) " )
assume A1: i <= 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
percases ( i < 0 or i = 0 ) by A1;
suppose i < 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
hence  h |^ i = (h |^ (abs i)) " by Def8; ::_thesis: verum
end;
supposeA2: i = 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
hence h |^ i = 1_ G by Lm3
.= (1_ G) " by Th8
.= (h |^ 0) " by Def7
.= (h |^ (abs i)) " by A2, ABSVALUE:def_1 ;
::_thesis: verum
end;
end;
end;

theorem :: GROUP_1:31
for i being Integer
for G being Group holds (1_ G) |^ i = 1_ G
proof
let i be Integer; ::_thesis: for G being Group holds (1_ G) |^ i = 1_ G
let G be Group; ::_thesis: (1_ G) |^ i = 1_ G
 ( (1_ G) |^ i = (1_ G) |^ (abs i) or ( (1_ G) |^ i = ((1_ G) |^ (abs i)) " & (1_ G) " = 1_ G ) ) by Def8, Th8;
hence  (1_ G) |^ i = 1_ G by Lm4; ::_thesis: verum
end;

theorem Th32: :: GROUP_1:32
for G being Group
for h being Element of G holds h |^ (- 1) = h "
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ (- 1) = h "
let h be Element of G; ::_thesis: h |^ (- 1) = h "
 abs (- 1) = - (- 1) by ABSVALUE:def_1;
hence h |^ (- 1) = (h |^ 1) " by Def8
.= h " by Th26 ;
::_thesis: verum
end;

Lm12:  for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
let G be Group; ::_thesis: for h being Element of G holds h |^ (- i) = (h |^ i) "
let h be Element of G; ::_thesis: h |^ (- i) = (h |^ i) "
percases ( i >= 0 or i < 0 ) ;
supposeA1: i >= 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
percases ( - i < - 0 or i = 0 ) by A1, XREAL_1:24;
supposeA2: - i < - 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
hence h |^ (- i) = (h |^ (abs (- i))) " by Def8
.= (h |^ (- (- i))) " by A2, ABSVALUE:def_1
.= (h |^ i) " ;
::_thesis: verum
end;
supposeA3: i = 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
hence h |^ (- i) = 1_ G by Lm3
.= (1_ G) " by Th8
.= (h |^ i) " by A3, Lm3 ;
::_thesis: verum
end;
end;
end;
supposeA4: i < 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
then  h |^ i = (h |^ (abs i)) " by Def8;
hence  h |^ (- i) = (h |^ i) " by A4, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;

Lm13:  for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
proof
let j be Integer; ::_thesis: ( j >= 1 or j = 0 or j < 0 )
 ( j < 0 or ( j is Element of NAT & ( j <> 0 or j = 0 ) ) ) by INT_1:3;
hence  ( j >= 1 or j = 0 or j < 0 ) by NAT_1:14; ::_thesis: verum
end;

Lm14:  for j being Integer
for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
proof
let j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let G be Group; ::_thesis: for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let h be Element of G; ::_thesis: h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
A1: now__::_thesis:_(h_|^_(j_-_1))_*_(h_*_(h_|^_(-_j)))_=_1__G
percases ( j >= 1 or j < 0 or j = 0 ) by Lm13;
supposeA2: j >= 1 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
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 ; ::_thesis: verum
end;
supposeA7: j < 0 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
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 ; ::_thesis: verum
end;
supposeA9: j = 0 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
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 ;
::_thesis: verum
end;
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  h |^ (j - 1) = (h |^ j) * (h |^ (- 1)) ; ::_thesis: verum
end;

Lm15:  for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
proof
let j be Integer; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
percases ( j >= 0 or j < 0 ) ;
suppose j >= 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
hence  ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
supposeA1: j < 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
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  ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
end;
end;

Lm16:  for j being Integer
for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
proof
let j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let G be Group; ::_thesis: for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let h be Element of G; ::_thesis: h |^ (j + 1) = (h |^ j) * (h |^ 1)
A1: now__::_thesis:_(h_|^_(j_+_1))_*_((h_|^_(-_1))_*_(h_|^_(-_j)))_=_1__G
percases ( j >= 0 or j < - 1 or j = - 1 ) by Lm15;
supposeA2: j >= 0 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
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 ;
::_thesis: verum
end;
suppose j < - 1 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
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 ;
::_thesis: verum
end;
supposeA5: j = - 1 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
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 ;
::_thesis: verum
end;
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) ; ::_thesis: verum
end;

theorem Th33: :: GROUP_1:33
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
proof
let i, j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let G be Group; ::_thesis: for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let h be Element of G; ::_thesis: h |^ (i + j) = (h |^ i) * (h |^ j)
defpred S1[ Integer] means  for i being Integer holds h |^ (i + $1) = (h |^ i) * (h |^ $1);
A1: for j being Integer st S1[j] holds
( S1[j - 1] & S1[j + 1] )
proof
let j be Integer; ::_thesis: ( S1[j] implies ( S1[j - 1] & S1[j + 1] ) )
assume A2: for i being Integer holds h |^ (i + j) = (h |^ i) * (h |^ j) ; ::_thesis: ( S1[j - 1] & S1[j + 1] )
thus  for i being Integer holds h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1)) ::_thesis: S1[j + 1]
proof
let i be Integer; ::_thesis: h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1))
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)) ; ::_thesis: verum
end;
let i be Integer; ::_thesis: h |^ (i + (j + 1)) = (h |^ i) * (h |^ (j + 1))
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 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let i be Integer; ::_thesis: h |^ (i + 0) = (h |^ i) * (h |^ 0)
thus h |^ (i + 0) = (h |^ i) * (1_ G) by Def4
.= (h |^ i) * (h |^ 0) by Def7 ; ::_thesis: verum
end;
 for j being Integer holds S1[j] from INT_1:sch_4(A3, A1);
hence  h |^ (i + j) = (h |^ i) * (h |^ j) ; ::_thesis: verum
end;

theorem :: GROUP_1:34
for i being Integer
for G being Group
for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let G be Group; ::_thesis: for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let h be Element of G; ::_thesis: ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
 h |^ 1 = h by Th26;
hence  ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) ) by Th33; ::_thesis: verum
end;

Lm17:  for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
let G be Group; ::_thesis: for h being Element of G holds (h ") |^ i = (h |^ i) "
let h be Element of G; ::_thesis: (h ") |^ i = (h |^ i) "
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: (h ") |^ i = (h |^ i) "
then reconsider n = i as Element of NAT by INT_1:3;
thus (h ") |^ i = (h |^ n) " by Lm8
.= (h |^ i) " ; ::_thesis: verum
end;
supposeA1: i < 0 ; ::_thesis: (h ") |^ i = (h |^ i) "
hence (h ") |^ i = ((h ") |^ (abs i)) " by Def8
.= ((h |^ (abs i)) ") " by Lm8
.= (h |^ i) " by A1, Def8 ;
::_thesis: verum
end;
end;
end;

theorem :: GROUP_1:35
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
proof
let i, j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
let G be Group; ::_thesis: for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
let h be Element of G; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ;
suppose ( i >= 0 & j >= 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
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 ; ::_thesis: verum
end;
suppose ( i >= 0 & j < 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
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 ;
::_thesis: verum
end;
suppose ( i < 0 & j >= 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
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 ;
::_thesis: verum
end;
suppose ( j < 0 & i < 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
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 ;
::_thesis: verum
end;
end;
end;

theorem :: GROUP_1:36
for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) " by Lm12;

theorem :: GROUP_1:37
for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) " by Lm17;

theorem Th38: :: GROUP_1:38
for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
proof
let i be Integer; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g * h) |^ i = (g |^ i) * (h |^ i) )
assume A1: g * h = h * g ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
percases ( i >= 0 or i < 0 ) ;
supposeA2: i >= 0 ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
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  (g * h) |^ i = (g |^ i) * (h |^ i) by A1, A3, Lm11; ::_thesis: verum
end;
supposeA4: i < 0 ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
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 ;
::_thesis: verum
end;
end;
end;

theorem Th39: :: GROUP_1:39
for i, j being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
proof
let i, j be Integer; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) )
assume A1: g * h = h * g ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( i < 0 & j < 0 ) ) ;
suppose ( i >= 0 & j >= 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
then  ( g |^ i = g |^ (abs i) & h |^ j = h |^ (abs j) ) by Def8;
hence  (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A1, Lm10; ::_thesis: verum
end;
supposeA2: ( i >= 0 & j < 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
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  (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A3, Th20; ::_thesis: verum
end;
supposeA4: ( i < 0 & j >= 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
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  (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A5, Th20; ::_thesis: verum
end;
suppose ( i < 0 & j < 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
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 ;
::_thesis: verum
end;
end;
end;

theorem :: GROUP_1:40
for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
proof
let i be Integer; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let g, h be Element of G; ::_thesis: ( g * h = h * g implies g * (h |^ i) = (h |^ i) * g )
assume A1: g * h = h * g ; ::_thesis: g * (h |^ i) = (h |^ i) * g
thus g * (h |^ i) = (g |^ 1) * (h |^ i) by Th26
.= (h |^ i) * (g |^ 1) by A1, Th39
.= (h |^ i) * g by Th26 ; ::_thesis: verum
end;

definition
let G be Group;
let h be Element of G;
attrh is being_of_order_0  means :Def10: :: GROUP_1:def 10
 for n being Nat st h |^ n = 1_ G holds
n = 0 ;
end;

:: deftheorem Def10 defines being_of_order_0 GROUP_1:def_10_:_
 for G being Group
for h being Element of G holds
( h is being_of_order_0 iff for n being Nat st h |^ n = 1_ G holds
n = 0 );

registration
let G be Group;
cluster 1_ G ->  non being_of_order_0 ;
coherence
 not 1_ G is being_of_order_0
proof
 (1_ G) |^ 8 = 1_ G by Lm4;
hence  not 1_ G is being_of_order_0 by Def10; ::_thesis: verum
end;
end;

definition
let G be Group;
let h be Element of G;
func ord h ->  Element of NAT  means :Def11: :: GROUP_1:def 11
it = 0  if h is being_of_order_0
otherwise ( h |^ it = 1_ G & it <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
it <= m ) );
existence
 ( ( h is being_of_order_0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not h is being_of_order_0 implies ex b1 being Element of NAT st
( h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b1 <= m ) ) ) )
proof
defpred S1[ 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 ) ; ::_thesis: ( not h is being_of_order_0 implies ex b1 being Element of NAT st
( h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b1 <= m ) ) )
hereby  ::_thesis: verum
assume  not h is being_of_order_0 ; ::_thesis: ex k being Element of NAT st
( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
then A1: ex n being Nat st S1[n] by Def10;
consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A1);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k = k; ::_thesis: ( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
thus  ( h |^ k = 1_ G & k <> 0 ) by A2; ::_thesis: for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m
let m be Nat; ::_thesis: ( h |^ m = 1_ G & m <> 0 implies k <= m )
assume  ( h |^ m = 1_ G & m <> 0 ) ; ::_thesis: k <= m
hence  k <= m by A3; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being Element of NAT holds
( ( h is being_of_order_0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not h is being_of_order_0 & h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b1 <= m ) & h |^ b2 = 1_ G & b2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b2 <= m ) implies b1 = b2 ) )
proof
let n1, n2 be Element of NAT ; ::_thesis: ( ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( not h is being_of_order_0 & h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 ) )
thus  ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; ::_thesis: ( not h is being_of_order_0 & h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume that
 not h is being_of_order_0 and
A4: ( h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) ) ; ::_thesis: n1 = n2
 ( n1 <= n2 & n2 <= n1 ) by A4;
hence  n1 = n2 by XXREAL_0:1; ::_thesis: verum
end;
correctness
consistency
for b1 being Element of NAT holds verum;
;
end;

:: deftheorem Def11 defines ord GROUP_1:def_11_:_
 for G being Group
for h being Element of G
for b3 being Element of NAT holds
( ( h is being_of_order_0 implies ( b3 = ord h iff b3 = 0 ) ) & ( not h is being_of_order_0 implies ( b3 = ord h iff ( h |^ b3 = 1_ G & b3 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b3 <= m ) ) ) ) );

theorem Th41: :: GROUP_1:41
for G being Group
for h being Element of G holds h |^ (ord h) = 1_ G
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ (ord h) = 1_ G
let h be Element of G; ::_thesis: h |^ (ord h) = 1_ G
percases ( h is being_of_order_0 or not h is being_of_order_0 ) ;
suppose h is being_of_order_0 ; ::_thesis: h |^ (ord h) = 1_ G
then  ord h = 0 by Def11;
hence  h |^ (ord h) = 1_ G by Def7; ::_thesis: verum
end;
suppose not h is being_of_order_0 ; ::_thesis: h |^ (ord h) = 1_ G
hence  h |^ (ord h) = 1_ G by Def11; ::_thesis: verum
end;
end;
end;

theorem :: GROUP_1:42
for G being Group holds ord (1_ G) = 1
proof
let G be Group; ::_thesis: ord (1_ G) = 1
A1: for n being Nat 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  ord (1_ G) = 1 by A1, Def11; ::_thesis: verum
end;

theorem :: GROUP_1:43
for G being Group
for h being Element of G st ord h = 1 holds
h = 1_ G
proof
let G be Group; ::_thesis: for h being Element of G st ord h = 1 holds
h = 1_ G
let h be Element of G; ::_thesis: ( ord h = 1 implies h = 1_ G )
assume A1: ord h = 1 ; ::_thesis: h = 1_ G
then  not h is being_of_order_0 by Def11;
then  h |^ 1 = 1_ G by A1, Def11;
hence  h = 1_ G by Th26; ::_thesis: verum
end;

theorem :: GROUP_1:44
for n being Nat
for G being Group
for h being Element of G st h |^ n = 1_ G holds
ord h divides n
proof
let n be Nat; ::_thesis: for G being Group
for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let G be Group; ::_thesis: for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let h be Element of G; ::_thesis: ( h |^ n = 1_ G implies ord h divides n )
defpred S1[ 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
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2: for k being Nat st k < n holds
S1[k] ; ::_thesis: S1[n]
assume A3: h |^ n = 1_ G ; ::_thesis: ord h divides n
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: ord h divides n
hence  ord h divides n by NAT_D:6; ::_thesis: verum
end;
supposeA4: n <> 0 ; ::_thesis: ord h divides n
percases ( ord h = 0 or ord h <> 0 ) ;
suppose ord h = 0 ; ::_thesis: ord h divides n
then  h is being_of_order_0 by Def11;
hence  ord h divides n by A3, A4, Def10; ::_thesis: verum
end;
supposeA5: ord h <> 0 ; ::_thesis: ord h divides n
then  not h is 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  ord h divides n by NAT_D:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
 for n being Nat holds S1[n] from NAT_1:sch_4(A1);
hence  ( h |^ n = 1_ G implies ord h divides n ) ; ::_thesis: verum
end;

definition
let G be finite 1-sorted ;
:: original: card
redefine func card G ->  Element of NAT ;
coherence
 card G is Element of NAT
proof
 card the carrier of G in NAT ;
hence  card G is Element of NAT ; ::_thesis: verum
end;
end;

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

definition
let IT be multMagma ;
attrIT is commutative  means :Def12: :: GROUP_1:def 12
 for x, y being Element of IT holds x * y = y * x;
end;

:: deftheorem Def12 defines commutative GROUP_1:def_12_:_
 for IT being multMagma holds
( IT is commutative iff for x, y being Element of IT holds x * y = y * x );

registration
cluster non empty strict unital Group-like associative commutative for multMagma ;
existence
 ex b1 being Group st
( b1 is strict & b1 is commutative )
proof
reconsider G0 = multMagma(# REAL,addreal #) as Group by Th3;
take  G0 ; ::_thesis: ( G0 is strict & G0 is commutative )
thus  G0 is strict ; ::_thesis: G0 is commutative
let a, g be Element of G0; :: according to GROUP_1:def_12 ::_thesis: a * g = g * a
reconsider A = a, B = g as Real ;
thus a * g = B + A by BINOP_2:def_9
.= g * a by BINOP_2:def_9 ; ::_thesis: verum
end;
end;

definition
let FS be non empty commutative multMagma ;
let x, y be Element of FS;
:: original: *
redefine funcx * y ->  Element of the carrier of FS;
commutativity
 for x, y being Element of FS holds x * y = y * x by Def12;
end;

theorem :: GROUP_1:46
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; :: according to GROUP_1:def_12 ::_thesis: h * g = g * h
reconsider A = h, B = g as Real ;
thus h * g = B + A by BINOP_2:def_9
.= g * h by BINOP_2:def_9 ; ::_thesis: verum
end;
hence  multMagma(# REAL,addreal #) is commutative Group ; ::_thesis: verum
end;


theorem :: GROUP_1:47
for A being commutative Group
for a, b being Element of A holds (a * b) " = (a ") * (b ") by Th17;

theorem :: GROUP_1:48
for i being Integer
for A being commutative Group
for a, b being Element of A holds (a * b) |^ i = (a |^ i) * (b |^ i) by Th38;

theorem :: GROUP_1:49
for A being commutative Group holds
( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )
proof
let A be commutative Group; ::_thesis: ( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )
set G = addLoopStr(# the carrier of A, the multF of A,(1_ A) #);
thus  addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian ::_thesis: ( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )
proof
let a, b be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of A ;
A1: for a, b being Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #)
for x, y being Element of A st a = x & b = y holds
a + b = x * y ;
thus a + b = x * y
.= b + a by A1 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )
let a, b, c be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); ::_thesis: (a + b) + c = a + (b + c)
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) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable
let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); ::_thesis: a + (0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)) = a
reconsider x = a as Element of A ;
thus a + (0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)) = x * (1_ A)
.= a by Def4 ; ::_thesis: verum
end;
let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
reconsider x = a as Element of A ;
reconsider b = (inverse_op A) . x as Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #) ;
take  b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)
thus a + b = x * (x ") by Def6
.= 0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #) by Def5 ; ::_thesis: verum
end;

begin

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

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

theorem :: GROUP_1:52
for L being non empty unital associative commutative multMagma
for x, y being Element of L
for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))
proof
let L be non empty unital associative commutative multMagma ; ::_thesis: for x, y being Element of L
for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))
let x, y be Element of L; ::_thesis: for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))
defpred S1[ Element of NAT ] means (power L) . ((x * y),$1) = ((power L) . (x,$1)) * ((power L) . (y,$1));
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
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  S1[n + 1] ; ::_thesis: verum
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: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;

definition
let G, H be multMagma ;
let IT be Function of G,H;
attrIT is unity-preserving  means :: GROUP_1:def 13
IT . (1_ G) = 1_ H;
end;

:: deftheorem  defines unity-preserving GROUP_1:def_13_:_
 for G, H being multMagma
for IT being Function of G,H holds
( IT is unity-preserving iff IT . (1_ G) = 1_ H );