:: Groups
:: by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990 Association of Mizar Users


begin

Lm1: now
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 ;
canceled;
attr IT is unital 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 );
attr IT is Group-like means :Def3: :: GROUP_1:def 3
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 :Def4: :: GROUP_1:def 4
for x, y, z being Element of IT holds (x * y) * z = x * (y * z);
end;

:: deftheorem GROUP_1:def 1 :
canceled;

:: deftheorem Def2 defines unital GROUP_1:def 2 :
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 Def3 defines Group-like GROUP_1:def 3 :
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 Def4 defines associative GROUP_1:def 4 :
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 multMagma ;
coherence
for b1 being multMagma st b1 is Group-like holds
b1 is unital
proof end;
end;

registration
cluster non empty strict Group-like associative multMagma ;
existence
ex b1 being multMagma st
( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty )
proof end;
end;

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

theorem :: GROUP_1:1
canceled;

theorem :: GROUP_1:2
canceled;

theorem :: GROUP_1:3
canceled;

theorem :: GROUP_1:4
canceled;

theorem :: GROUP_1:5
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 Def3, Def4;

theorem :: GROUP_1:6
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 end;

theorem Th7: :: GROUP_1:7
( multMagma(# REAL,addreal #) is associative & multMagma(# REAL,addreal #) is Group-like )
proof end;

definition
let G be multMagma ;
assume A1: G is unital ;
func 1_ G -> Element of G means :Def5: :: GROUP_1:def 5
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, Def2;
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 end;
end;

:: deftheorem Def5 defines 1_ GROUP_1:def 5 :
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:8
canceled;

theorem :: GROUP_1:9
canceled;

theorem :: GROUP_1:10
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 Def5;

definition
let G be Group;
let h be Element of G;
func h " -> Element of G means :Def6: :: GROUP_1:def 6
( 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 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 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 Def6 defines " GROUP_1:def 6 :
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:11
canceled;

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

theorem :: GROUP_1:13
canceled;

theorem Th14: :: GROUP_1:14
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 end;

theorem :: GROUP_1:15
for G being Group
for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
proof end;

theorem Th16: :: GROUP_1:16
for G being Group holds (1_ G) " = 1_ G
proof end;

theorem :: GROUP_1:17
for G being Group
for h, g being Element of G st h " = g " holds
h = g
proof end;

theorem :: GROUP_1:18
for G being Group
for h being Element of G st h " = 1_ G holds
h = 1_ G
proof end;

theorem :: GROUP_1:19
for G being Group
for h being Element of G holds (h ") " = h ;

theorem Th20: :: GROUP_1:20
for G being Group
for h, g being Element of G st h * g = 1_ G holds
( h = g " & g = h " )
proof end;

theorem Th21: :: GROUP_1:21
for G being Group
for h, f, g being Element of G holds
( h * f = g iff f = (h ") * g )
proof end;

theorem Th22: :: GROUP_1:22
for G being Group
for f, h, g being Element of G holds
( f * h = g iff f = g * (h ") )
proof end;

theorem :: GROUP_1:23
for G being Group
for g, h being Element of G ex f being Element of G st g * f = h
proof end;

theorem :: GROUP_1:24
for G being Group
for g, h being Element of G ex f being Element of G st f * g = h
proof end;

theorem Th25: :: GROUP_1:25
for G being Group
for h, g being Element of G holds (h * g) " = (g ") * (h ")
proof end;

theorem Th26: :: GROUP_1:26
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
proof end;

theorem Th27: :: GROUP_1:27
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
proof end;

theorem Th28: :: GROUP_1:28
for G being Group
for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
proof end;

definition
let G be Group;
func inverse_op G -> UnOp of G means :Def7: :: GROUP_1:def 7
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 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 end;
end;

:: deftheorem Def7 defines inverse_op GROUP_1:def 7 :
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 " );

theorem :: GROUP_1:29
canceled;

theorem :: GROUP_1:30
canceled;

theorem :: GROUP_1:31
canceled;

registration
let G be non empty associative multMagma ;
cluster the multF of G -> associative ;
coherence
the multF of G is associative
proof end;
end;

theorem Th32: :: GROUP_1:32
for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G
proof end;

theorem Th33: :: GROUP_1:33
for G being non empty unital multMagma holds the_unity_wrt the multF of G = 1_ G
proof end;

theorem :: GROUP_1:34
canceled;

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 end;
end;

theorem Th35: :: GROUP_1:35
for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G
proof end;

theorem :: GROUP_1:36
canceled;

registration
let G be Group;
cluster the multF of G -> having_an_inverseOp ;
coherence
the multF of G is having_an_inverseOp
proof end;
end;

theorem :: GROUP_1:37
for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G
proof end;

definition
let G be non empty multMagma ;
func power G -> Function of [: the carrier of G,NAT:], the carrier of G means :Def8: :: GROUP_1:def 8
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 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 end;
end;

:: deftheorem Def8 defines power GROUP_1:def 8 :
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;
func h |^ i -> Element of G equals :Def9: :: GROUP_1:def 9
(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 Def9 defines |^ GROUP_1:def 9 :
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 10
(power G) . (h,n);
compatibility
for b1 being Element of G holds
( b1 = h |^ n iff b1 = (power G) . (h,n) )
proof end;
end;

:: deftheorem defines |^ GROUP_1:def 10 :
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 end;

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

theorem :: GROUP_1:38
canceled;

theorem :: GROUP_1:39
canceled;

theorem :: GROUP_1:40
canceled;

theorem :: GROUP_1:41
canceled;

theorem :: GROUP_1:42
canceled;

Lm4: for n being Nat
for G being Group holds (1_ G) |^ n = 1_ G
proof end;

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

theorem Th44: :: GROUP_1:44
for G being Group
for h being Element of G holds h |^ 1 = h
proof end;

theorem Th45: :: GROUP_1:45
for G being Group
for h being Element of G holds h |^ 2 = h * h
proof end;

theorem :: GROUP_1:46
for G being Group
for h being Element of G holds h |^ 3 = (h * h) * h
proof end;

theorem :: GROUP_1:47
for G being Group
for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
proof end;

theorem :: GROUP_1:48
canceled;

theorem :: GROUP_1:49
canceled;

theorem :: GROUP_1:50
canceled;

theorem :: GROUP_1:51
canceled;

theorem :: GROUP_1:52
canceled;

theorem :: GROUP_1:53
canceled;

theorem :: GROUP_1:54
canceled;

theorem :: GROUP_1:55
canceled;

theorem :: GROUP_1:56
canceled;

theorem :: GROUP_1:57
canceled;

theorem :: GROUP_1:58
canceled;

theorem :: GROUP_1:59
canceled;

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 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 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 end;

Lm8: for n being Nat
for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
proof 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 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 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 end;

theorem Th60: :: GROUP_1:60
for i being Integer
for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
proof end;

theorem :: GROUP_1:61
for i being Integer
for G being Group holds (1_ G) |^ i = 1_ G
proof end;

theorem Th62: :: GROUP_1:62
for G being Group
for h being Element of G holds h |^ (- 1) = h "
proof end;

Lm12: for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
proof end;

Lm13: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
proof 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 end;

Lm15: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
proof 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 end;

theorem Th63: :: GROUP_1:63
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
proof end;

theorem :: GROUP_1:64
canceled;

theorem :: GROUP_1:65
canceled;

theorem :: GROUP_1:66
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 end;

Lm17: for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
proof end;

theorem :: GROUP_1:67
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
proof end;

theorem :: GROUP_1:68
canceled;

theorem :: GROUP_1:69
canceled;

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

theorem :: GROUP_1:71
canceled;

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

theorem Th73: :: GROUP_1:73
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 end;

theorem Th74: :: GROUP_1:74
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 end;

theorem :: GROUP_1:75
canceled;

theorem :: GROUP_1:76
canceled;

theorem :: GROUP_1:77
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 end;

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

:: deftheorem Def11 defines being_of_order_0 GROUP_1:def 11 :
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 );

theorem :: GROUP_1:78
canceled;

theorem :: GROUP_1:79
canceled;

registration
let G be Group;
cluster 1_ G -> non being_of_order_0 ;
coherence
not 1_ G is being_of_order_0
proof end;
end;

definition
let G be Group;
let h be Element of G;
func ord h -> Element of NAT means :Def12: :: GROUP_1:def 12
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 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 end;
correctness
consistency
for b1 being Element of NAT holds verum
;
;
end;

:: deftheorem Def12 defines ord GROUP_1:def 12 :
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 :: GROUP_1:80
canceled;

theorem :: GROUP_1:81
canceled;

theorem Th82: :: GROUP_1:82
for G being Group
for h being Element of G holds h |^ (ord h) = 1_ G
proof end;

theorem :: GROUP_1:83
canceled;

theorem :: GROUP_1:84
for G being Group holds ord (1_ G) = 1
proof end;

theorem :: GROUP_1:85
for G being Group
for h being Element of G st ord h = 1 holds
h = 1_ G
proof end;

theorem :: GROUP_1:86
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 end;

definition
let G be finite 1-sorted ;
canceled;
:: original: card
redefine func card G -> Element of NAT ;
coherence
card G is Element of NAT
proof end;
end;

:: deftheorem GROUP_1:def 13 :
canceled;

theorem :: GROUP_1:87
canceled;

theorem :: GROUP_1:88
canceled;

theorem :: GROUP_1:89
canceled;

theorem :: GROUP_1:90
for G being non empty finite 1-sorted holds card G >= 1
proof end;

definition
canceled;
canceled;
let IT be multMagma ;
attr IT is commutative means :Def16: :: GROUP_1:def 16
for x, y being Element of IT holds x * y = y * x;
end;

:: deftheorem GROUP_1:def 14 :
canceled;

:: deftheorem GROUP_1:def 15 :
canceled;

:: deftheorem Def16 defines commutative GROUP_1:def 16 :
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 multMagma ;
existence
ex b1 being Group st
( b1 is strict & b1 is commutative )
proof end;
end;

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

theorem :: GROUP_1:91
canceled;

theorem :: GROUP_1:92
multMagma(# REAL,addreal #) is commutative Group
proof end;

theorem :: GROUP_1:93
canceled;

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

theorem :: GROUP_1:95
canceled;

theorem :: GROUP_1:96
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 Th73;

theorem :: GROUP_1:97
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 end;

begin

theorem Th98: :: GROUP_1:98
for L being non empty unital multMagma
for x being Element of L holds (power L) . (x,1) = x
proof end;

theorem :: GROUP_1:99
for L being non empty unital multMagma
for x being Element of L holds (power L) . (x,2) = x * x
proof end;

theorem :: GROUP_1:100
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 end;

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

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