begin
:: deftheorem Def1 defines solvable GRSOLV_1:def 1 :
for IT being Group holds
( IT is solvable iff ex F being FinSequence of Subgroups IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) ) );
theorem Th1:
theorem
theorem
theorem Th4:
theorem
theorem
theorem
:: deftheorem defines | GRSOLV_1:def 2 :
for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g | A = g | the carrier of A;
:: deftheorem defines .: GRSOLV_1:def 3 :
for G, H being strict Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g .: A = Image (g | A);
theorem
canceled;
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem