begin
theorem Th1:
for
G being
Group for
a,
b being
Element of
G holds
(
(a * b) * (b ") = a &
(a * (b ")) * b = a &
((b ") * b) * a = a &
(b * (b ")) * a = a &
a * (b * (b ")) = a &
a * ((b ") * b) = a &
(b ") * (b * a) = a &
b * ((b ") * a) = a )
Lm1:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
Lm4:
for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n
Lm5:
for G being Group
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)