begin
theorem Th1:
for
G being
Group for
a,
b being
Element of 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 holds a * b = b * a
;
theorem
theorem
theorem Th4:
theorem
theorem Th6:
theorem
theorem
theorem
canceled;
theorem Th10:
theorem
theorem
theorem
theorem
canceled;
theorem
:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th19:
:: deftheorem defines |^ GROUP_3:def 2 :
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
canceled;
theorem Th32:
Lm4:
for n being Nat
for G being Group
for a, b being Element of holds (a |^ n) |^ b = (a |^ b) |^ n
theorem
theorem
theorem Th35:
theorem Th36:
:: deftheorem defines |^ GROUP_3:def 3 :
theorem
canceled;
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem
theorem
theorem
:: deftheorem defines |^ GROUP_3:def 4 :
:: deftheorem defines |^ GROUP_3:def 5 :
theorem
canceled;
theorem
canceled;
theorem Th50:
theorem Th51:
theorem
theorem
theorem
theorem
theorem Th56:
theorem
theorem
theorem Th59:
theorem
theorem Th61:
theorem
theorem Th63:
theorem
canceled;
theorem Th65:
theorem
theorem
:: deftheorem Def6 defines |^ GROUP_3:def 6 :
theorem
canceled;
theorem
canceled;
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem
canceled;
theorem Th76:
theorem Th77:
theorem Th78:
theorem
theorem Th80:
theorem
theorem Th82:
theorem
theorem Th84:
theorem
theorem Th86:
:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :
theorem
canceled;
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
:: deftheorem defines con_class GROUP_3:def 8 :
theorem
canceled;
theorem Th95:
theorem Th96:
theorem Th97:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :
theorem
canceled;
theorem Th104:
theorem Th105:
theorem Th106:
theorem Th107:
theorem Th108:
theorem Th109:
:: deftheorem defines con_class GROUP_3:def 10 :
theorem
canceled;
theorem
theorem
canceled;
theorem Th113:
theorem
theorem
theorem
theorem
theorem Th118:
theorem
:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :
theorem
canceled;
theorem Th121:
theorem Th122:
theorem Th123:
theorem Th124:
:: deftheorem Def12 defines con_class GROUP_3:def 12 :
theorem
canceled;
theorem
canceled;
theorem Th127:
theorem Th128:
theorem Th129:
theorem Th130:
theorem
theorem
theorem
theorem Th134:
:: deftheorem Def13 defines normal GROUP_3:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th137:
theorem
theorem
theorem Th140:
theorem Th141:
theorem Th142:
theorem
theorem
theorem
theorem
theorem
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)
theorem Th148:
theorem
theorem
theorem
:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :
theorem
canceled;
theorem
canceled;
theorem Th154:
theorem Th155:
theorem
theorem Th157:
theorem
:: deftheorem defines Normalizator GROUP_3:def 15 :
theorem
canceled;
theorem Th160:
theorem Th161:
theorem
theorem Th163:
theorem
theorem