:: 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 b₁ being multMagma st b₁ is Group-like holds
b₁ is unital

proof end;

end;

registration

cluster non empty strict Group-like associative multMagma ;
existence
ex b₁ being multMagma st
( b₁ is strict & b₁ is Group-like & b₁ is associative & not b₁ 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 b₁ being Element of G st
for h being Element of G holds
( h * b₁ = h & b₁ * h = h ) by A1, Def2;
uniqueness
for b₁, b₂ being Element of G st ( for h being Element of G holds
( h * b₁ = h & b₁ * h = h ) ) & ( for h being Element of G holds
( h * b₂ = h & b₂ * h = h ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines 1_ GROUP_1:def 5 :
for G being multMagma st G is unital holds
for b₂ being Element of G holds
( b₂ = 1_ G iff for h being Element of G holds
( h * b₂ = h & b₂ * 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 b₁ being Element of G st
( h * b₁ = 1_ G & b₁ * h = 1_ G )

proof end;

uniqueness
for b₁, b₂ being Element of G st h * b₁ = 1_ G & b₁ * h = 1_ G & h * b₂ = 1_ G & b₂ * h = 1_ G holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Element of G st b₂ * b₁ = 1_ G & b₁ * b₂ = 1_ G holds
( b₁ * b₂ = 1_ G & b₂ * b₁ = 1_ G ) ;

end;

:: deftheorem Def6 defines " GROUP_1:def 6 :
for G being Group
for h, b₃ being Element of G holds
( b₃ = h " iff ( h * b₃ = 1_ G & b₃ * 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 b₁ being UnOp of G st
for h being Element of G holds b₁ . h = h "

proof end;

uniqueness
for b₁, b₂ being UnOp of G st ( for h being Element of G holds b₁ . h = h " ) & ( for h being Element of G holds b₂ . h = h " ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines inverse_op GROUP_1:def 7 :
for G being Group
for b₂ being UnOp of G holds
( b₂ = inverse_op G iff for h being Element of G holds b₂ . 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 b₁ being Function of [: the carrier of G,NAT:], the carrier of G st
for h being Element of G holds
( b₁ . (h,0) = 1_ G & ( for n being Element of NAT holds b₁ . (h,(n + 1)) = (b₁ . (h,n)) * h ) )

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds
( b₁ . (h,0) = 1_ G & ( for n being Element of NAT holds b₁ . (h,(n + 1)) = (b₁ . (h,n)) * h ) ) ) & ( for h being Element of G holds
( b₂ . (h,0) = 1_ G & ( for n being Element of NAT holds b₂ . (h,(n + 1)) = (b₂ . (h,n)) * h ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines power GROUP_1:def 8 :
for G being non empty multMagma
for b₂ being Function of [: the carrier of G,NAT:], the carrier of G holds
( b₂ = power G iff for h being Element of G holds
( b₂ . (h,0) = 1_ G & ( for n being Element of NAT holds b₂ . (h,(n + 1)) = (b₂ . (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 b₁ 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 b₁ being Element of G holds
( b₁ = h |^ n iff b₁ = (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 b₁ being Element of NAT st b₁ = 0 ) & ( not h is being_of_order_0 implies ex b₁ being Element of NAT st
( h |^ b₁ = 1_ G & b₁ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₁ <= m ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT holds
( ( h is being_of_order_0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not h is being_of_order_0 & h |^ b₁ = 1_ G & b₁ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₁ <= m ) & h |^ b₂ = 1_ G & b₂ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₂ <= m ) implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ 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 b₃ being Element of NAT holds
( ( h is being_of_order_0 implies ( b₃ = ord h iff b₃ = 0 ) ) & ( not h is being_of_order_0 implies ( b₃ = ord h iff ( h |^ b₃ = 1_ G & b₃ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₃ <= 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 b₁ being Group st
( b₁ is strict & b₁ 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 );