begin
Lm1:
for x being set
for G being non empty 1-sorted
for A being Subset of st x in A holds
x is Element of
;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines " GROUP_2:def 1 :
theorem
canceled;
theorem Th5:
theorem
theorem
theorem
theorem
theorem Th10:
:: deftheorem defines * GROUP_2:def 2 :
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem
theorem Th26:
theorem Th27:
theorem
Lm2:
for A being commutative Group
for a, b being Element of holds a * b = b * a
;
theorem Th29:
theorem
:: deftheorem defines * GROUP_2:def 3 :
:: deftheorem defines * GROUP_2:def 4 :
theorem
canceled;
theorem
canceled;
theorem Th33:
theorem Th34:
theorem
theorem
theorem
theorem Th38:
theorem
theorem Th40:
theorem
theorem
theorem Th43:
theorem
:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem
theorem Th57:
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
:: deftheorem defines = GROUP_2:def 6 :
theorem Th70:
theorem Th71:
:: deftheorem Def7 defines (1). GROUP_2:def 7 :
:: deftheorem defines (Omega). GROUP_2:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th75:
theorem
theorem Th77:
theorem
theorem
theorem Th80:
theorem Th81:
theorem Th82:
theorem
theorem
theorem
:: deftheorem defines carr GROUP_2:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th89:
theorem Th90:
theorem
theorem
theorem Th93:
theorem
:: deftheorem Def10 defines /\ GROUP_2:def 10 :
theorem
canceled;
theorem
canceled;
theorem Th97:
theorem
theorem Th99:
theorem
theorem Th101:
theorem
Lm3:
for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2),the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1,the multF of H1 #) )
theorem
theorem
theorem
Lm4:
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines * GROUP_2:def 11 :
:: deftheorem defines * GROUP_2:def 12 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines * GROUP_2:def 13 :
:: deftheorem defines * GROUP_2:def 14 :
theorem
canceled;
theorem
canceled;
theorem Th125:
theorem Th126:
theorem
theorem
theorem
theorem Th130:
theorem
canceled;
theorem
theorem Th133:
theorem Th134:
theorem
theorem Th136:
theorem Th137:
theorem Th138:
theorem Th139:
theorem
theorem
theorem Th142:
theorem Th143:
theorem
theorem Th145:
theorem
theorem
theorem
theorem
theorem
theorem Th151:
theorem Th152:
theorem Th153:
theorem Th154:
theorem
theorem Th156:
:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :
:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th166:
theorem Th167:
theorem Th168:
theorem
theorem
theorem
theorem Th172:
theorem Th173:
theorem
:: deftheorem defines Index GROUP_2:def 17 :
theorem
:: deftheorem Def18 defines index GROUP_2:def 18 :
theorem
Lm5:
for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )
theorem Th177:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th184:
theorem
theorem