:: The {J}ordan-H\"older Theorem
:: by Marco Riccardi
::
:: Received April 20, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

:: ALG I.3.2 Definition 2
definition
let O, E be set ;
let A be Action of O,E;
let IT be set ;
pred IT is_stable_under_the_action_of A means :Def1: :: GROUP_9:def 1
for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: IT c= IT;
end;

:: deftheorem Def1 defines is_stable_under_the_action_of GROUP_9:def 1 :
for O, E being set
for A being Action of O,E
for IT being set holds
( IT is_stable_under_the_action_of A iff for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: IT c= IT );

Lm1: for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A

proof end;

definition
let O, E be set ;
let A be Action of O,E;
let X be Subset of E;
func the_stable_subset_generated_by (X,A) -> Subset of E means :Def2: :: GROUP_9:def 2
( X c= it & it is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
it c= Y ) );
existence
ex b1 being Subset of E st
( X c= b1 & b1 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
b1 c= Y ) )
proof end;
uniqueness
for b1, b2 being Subset of E st X c= b1 & b1 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
b1 c= Y ) & X c= b2 & b2 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
b2 c= Y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines the_stable_subset_generated_by GROUP_9:def 2 :
for O, E being set
for A being Action of O,E
for X, b5 being Subset of E holds
( b5 = the_stable_subset_generated_by (X,A) iff ( X c= b5 & b5 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
b5 c= Y ) ) );

definition
let O, E be set ;
let A be Action of O,E;
let F be FinSequence of O;
func Product (F,A) -> Function of E,E means :Def3: :: GROUP_9:def 3
it = id E if len F = 0
otherwise ex PF being FinSequence of Funcs (E,E) st
( it = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) );
existence
( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st
( b1 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of E,E holds
( ( len F = 0 & b1 = id E & b2 = id E implies b1 = b2 ) & ( not len F = 0 & ex PF being FinSequence of Funcs (E,E) st
( b1 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) & ex PF being FinSequence of Funcs (E,E) st
( b2 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) implies b1 = b2 ) )
proof end;
consistency
for b1 being Function of E,E holds verum
;
end;

:: deftheorem Def3 defines Product GROUP_9:def 3 :
for O, E being set
for A being Action of O,E
for F being FinSequence of O
for b5 being Function of E,E holds
( ( len F = 0 implies ( b5 = Product (F,A) iff b5 = id E ) ) & ( not len F = 0 implies ( b5 = Product (F,A) iff ex PF being FinSequence of Funcs (E,E) st
( b5 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) );

:: ALG I.3.4 Definition 6
definition
let O be set ;
let G be Group;
let IT be Action of O, the carrier of G;
attr IT is distributive means :Def4: :: GROUP_9:def 4
for o being Element of O st o in O holds
IT . o is Homomorphism of G,G;
end;

:: deftheorem Def4 defines distributive GROUP_9:def 4 :
for O being set
for G being Group
for IT being Action of O, the carrier of G holds
( IT is distributive iff for o being Element of O st o in O holds
IT . o is Homomorphism of G,G );

definition
let O be set ;
attr c2 is strict ;
struct HGrWOpStr over O -> multMagma ;
aggr HGrWOpStr(# carrier, multF, action #) -> HGrWOpStr over O;
sel action c2 -> Action of O, the carrier of c2;
end;

registration
let O be set ;
cluster non empty for HGrWOpStr over O;
existence
not for b1 being HGrWOpStr over O holds b1 is empty
proof end;
end;

definition
let O be set ;
let IT be non empty HGrWOpStr over O;
attr IT is distributive means :Def5: :: GROUP_9:def 5
for G being Group
for a being Action of O, the carrier of G st a = the action of IT & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of IT, the multF of IT #) holds
a is distributive ;
end;

:: deftheorem Def5 defines distributive GROUP_9:def 5 :
for O being set
for IT being non empty HGrWOpStr over O holds
( IT is distributive iff for G being Group
for a being Action of O, the carrier of G st a = the action of IT & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of IT, the multF of IT #) holds
a is distributive );

Lm2: for O, E being set holds [:O,{(id E)}:] is Action of O,E
proof end;

Lm3: for O being set
for G being strict Group ex H being non empty HGrWOpStr over O st
( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

proof end;

registration
let O be set ;
cluster non empty Group-like associative strict distributive for HGrWOpStr over O;
existence
ex b1 being non empty HGrWOpStr over O st
( b1 is strict & b1 is distributive & b1 is Group-like & b1 is associative )
proof end;
end;

:: ALG I.4.2 Definition 2
definition
let O be set ;
mode GroupWithOperators of O is non empty Group-like associative distributive HGrWOpStr over O;
end;

definition
let O be set ;
let G be GroupWithOperators of O;
let o be Element of O;
func G ^ o -> Homomorphism of G,G equals :Def6: :: GROUP_9:def 6
the action of G . o if o in O
otherwise id the carrier of G;
correctness
coherence
( ( o in O implies the action of G . o is Homomorphism of G,G ) & ( not o in O implies id the carrier of G is Homomorphism of G,G ) )
;
consistency
for b1 being Homomorphism of G,G holds verum
;
proof end;
end;

:: deftheorem Def6 defines ^ GROUP_9:def 6 :
for O being set
for G being GroupWithOperators of O
for o being Element of O holds
( ( o in O implies G ^ o = the action of G . o ) & ( not o in O implies G ^ o = id the carrier of G ) );

definition
let O be set ;
let G be GroupWithOperators of O;
mode StableSubgroup of G -> non empty Group-like associative distributive HGrWOpStr over O means :Def7: :: GROUP_9:def 7
( it is Subgroup of G & ( for o being Element of O holds it ^ o = (G ^ o) | the carrier of it ) );
correctness
existence
ex b1 being non empty Group-like associative distributive HGrWOpStr over O st
( b1 is Subgroup of G & ( for o being Element of O holds b1 ^ o = (G ^ o) | the carrier of b1 ) )
;
proof end;
end;

:: deftheorem Def7 defines StableSubgroup GROUP_9:def 7 :
for O being set
for G being GroupWithOperators of O
for b3 being non empty Group-like associative distributive HGrWOpStr over O holds
( b3 is StableSubgroup of G iff ( b3 is Subgroup of G & ( for o being Element of O holds b3 ^ o = (G ^ o) | the carrier of b3 ) ) );

Lm4: for O being set
for G being GroupWithOperators of O holds HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G

proof end;

registration
let O be set ;
let G be GroupWithOperators of O;
cluster non empty unital Group-like associative strict distributive for StableSubgroup of G;
correctness
existence
ex b1 being StableSubgroup of G st b1 is strict
;
proof end;
end;

Lm5: for O being set
for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2

proof end;

definition
let O be set ;
let G be GroupWithOperators of O;
func (1). G -> strict StableSubgroup of G means :Def8: :: GROUP_9:def 8
the carrier of it = {(1_ G)};
existence
ex b1 being strict StableSubgroup of G st the carrier of b1 = {(1_ G)}
proof end;
uniqueness
for b1, b2 being strict StableSubgroup of G st the carrier of b1 = {(1_ G)} & the carrier of b2 = {(1_ G)} holds
b1 = b2
by Lm5;
end;

:: deftheorem Def8 defines (1). GROUP_9:def 8 :
for O being set
for G being GroupWithOperators of O
for b3 being strict StableSubgroup of G holds
( b3 = (1). G iff the carrier of b3 = {(1_ G)} );

definition
let O be set ;
let G be GroupWithOperators of O;
func (Omega). G -> strict StableSubgroup of G equals :: GROUP_9:def 9
HGrWOpStr(# the carrier of G, the multF of G, the action of G #);
correctness
coherence
HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is strict StableSubgroup of G
;
by Lm4;
end;

:: deftheorem defines (Omega). GROUP_9:def 9 :
for O being set
for G being GroupWithOperators of O holds (Omega). G = HGrWOpStr(# the carrier of G, the multF of G, the action of G #);

definition
let O be set ;
let G be GroupWithOperators of O;
let IT be StableSubgroup of G;
attr IT is normal means :Def10: :: GROUP_9:def 10
for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds
H is normal ;
end;

:: deftheorem Def10 defines normal GROUP_9:def 10 :
for O being set
for G being GroupWithOperators of O
for IT being StableSubgroup of G holds
( IT is normal iff for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds
H is normal );

registration
let O be set ;
let G be GroupWithOperators of O;
cluster non empty unital Group-like associative strict distributive normal for StableSubgroup of G;
existence
ex b1 being StableSubgroup of G st
( b1 is strict & b1 is normal )
proof end;
end;

registration
let O be set ;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
cluster non empty unital Group-like associative distributive normal for StableSubgroup of H;
existence
ex b1 being StableSubgroup of H st b1 is normal
proof end;
end;

registration
let O be set ;
let G be GroupWithOperators of O;
cluster (1). G -> strict normal ;
correctness
coherence
(1). G is normal
;
proof end;
cluster (Omega). G -> strict normal ;
correctness
coherence
(Omega). G is normal
;
proof end;
end;

definition
let O be set ;
let G be GroupWithOperators of O;
func the_stable_subgroups_of G -> set means :Def11: :: GROUP_9:def 11
for x being set holds
( x in it iff x is strict StableSubgroup of G );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict StableSubgroup of G )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict StableSubgroup of G ) ) & ( for x being set holds
( x in b2 iff x is strict StableSubgroup of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines the_stable_subgroups_of GROUP_9:def 11 :
for O being set
for G being GroupWithOperators of O
for b3 being set holds
( b3 = the_stable_subgroups_of G iff for x being set holds
( x in b3 iff x is strict StableSubgroup of G ) );

registration
let O be set ;
let G be GroupWithOperators of O;
cluster the_stable_subgroups_of G -> non empty ;
correctness
coherence
not the_stable_subgroups_of G is empty
;
proof end;
end;

definition
let IT be Group;
attr IT is simple means :Def12: :: GROUP_9:def 12
( not IT is trivial & ( for H being strict normal Subgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) );
end;

:: deftheorem Def12 defines simple GROUP_9:def 12 :
for IT being Group holds
( IT is simple iff ( not IT is trivial & ( for H being strict normal Subgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

Lm6: Group_of_Perm 2 is simple
proof end;

registration
cluster non empty strict unital Group-like associative simple for multMagma ;
existence
ex b1 being Group st
( b1 is strict & b1 is simple )
by Lm6;
end;

:: ALG I.4.4 Definition 7
definition
let O be set ;
let IT be GroupWithOperators of O;
attr IT is simple means :Def13: :: GROUP_9:def 13
( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) );
end;

:: deftheorem Def13 defines simple GROUP_9:def 13 :
for O being set
for IT being GroupWithOperators of O holds
( IT is simple iff ( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

Lm7: for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

proof end;

Lm8: for G1, G2 being Group
for A1 being Subset of G1
for A2 being Subset of G2
for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )

proof end;

registration
let O be set ;
cluster non empty unital Group-like associative strict distributive simple for HGrWOpStr over O;
existence
ex b1 being GroupWithOperators of O st
( b1 is strict & b1 is simple )
proof end;
end;

definition
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func Cosets N -> set means :Def14: :: GROUP_9:def 14
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = Cosets H;
existence
ex b1 being set st
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = Cosets H
proof end;
uniqueness
for b1, b2 being set st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = Cosets H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b2 = Cosets H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Cosets GROUP_9:def 14 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b4 being set holds
( b4 = Cosets N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b4 = Cosets H );

definition
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosOp N -> BinOp of (Cosets N) means :Def15: :: GROUP_9:def 15
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = CosOp H;
existence
ex b1 being BinOp of (Cosets N) st
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = CosOp H
proof end;
uniqueness
for b1, b2 being BinOp of (Cosets N) st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = CosOp H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b2 = CosOp H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines CosOp GROUP_9:def 15 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b4 being BinOp of (Cosets N) holds
( b4 = CosOp N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b4 = CosOp H );

Lm9: for G being Group
for N being normal Subgroup of G
for A being Element of Cosets N
for g being Element of G holds
( g in A iff A = g * N )

proof end;

Lm10: for O being set
for o being Element of O
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
(G ^ o) . g in H

proof end;

definition
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosAc N -> Action of O,(Cosets N) means :Def16: :: GROUP_9:def 16
for o being Element of O holds it . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g )
}
if not O is empty
otherwise it = [:{},{(id (Cosets N))}:];
existence
( ( not O is empty implies ex b1 being Action of O,(Cosets N) st
for o being Element of O holds b1 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g )
}
) & ( O is empty implies ex b1 being Action of O,(Cosets N) st b1 = [:{},{(id (Cosets N))}:] ) )
proof end;
uniqueness
for b1, b2 being Action of O,(Cosets N) holds
( ( not O is empty & ( for o being Element of O holds b1 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g )
}
) & ( for o being Element of O holds b2 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g )
}
) implies b1 = b2 ) & ( O is empty & b1 = [:{},{(id (Cosets N))}:] & b2 = [:{},{(id (Cosets N))}:] implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Action of O,(Cosets N) holds verum
;
;
end;

:: deftheorem Def16 defines CosAc GROUP_9:def 16 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b4 being Action of O,(Cosets N) holds
( ( not O is empty implies ( b4 = CosAc N iff for o being Element of O holds b4 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g )
}
) ) & ( O is empty implies ( b4 = CosAc N iff b4 = [:{},{(id (Cosets N))}:] ) ) );

definition
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func G ./. N -> HGrWOpStr over O equals :: GROUP_9:def 17
HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);
correctness
coherence
HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #) is HGrWOpStr over O
;
;
end;

:: deftheorem defines ./. GROUP_9:def 17 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds G ./. N = HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);

registration
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
cluster G ./. N -> non empty ;
correctness
coherence
not G ./. N is empty
;
proof end;
cluster G ./. N -> Group-like associative distributive ;
correctness
coherence
( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative )
;
proof end;
end;

:: ALG I.4.2 Definition 3
definition
let O be set ;
let G, H be GroupWithOperators of O;
let f be Function of G,H;
attr f is homomorphic means :Def18: :: GROUP_9:def 18
for o being Element of O
for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g);
end;

:: deftheorem Def18 defines homomorphic GROUP_9:def 18 :
for O being set
for G, H being GroupWithOperators of O
for f being Function of G,H holds
( f is homomorphic iff for o being Element of O
for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g) );

registration
let O be set ;
let G, H be GroupWithOperators of O;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total multiplicative homomorphic for Element of bool [: the carrier of G, the carrier of H:];
existence
ex b1 being Function of G,H st
( b1 is multiplicative & b1 is homomorphic )
proof end;
end;

definition
let O be set ;
let G, H be GroupWithOperators of O;
mode Homomorphism of G,H is multiplicative homomorphic Function of G,H;
end;

Lm11: for O being set
for G, H, I being GroupWithOperators of O
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

proof end;

definition
let O be set ;
let G, H, I be GroupWithOperators of O;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
:: original: *
redefine func h1 * h -> Homomorphism of G,I;
correctness
coherence
h * h1 is Homomorphism of G,I
;
by Lm11;
end;

definition
let O be set ;
let G, H be GroupWithOperators of O;
pred G,H are_isomorphic means :Def19: :: GROUP_9:def 19
ex h being Homomorphism of G,H st h is bijective ;
reflexivity
for G being GroupWithOperators of O ex h being Homomorphism of G,G st h is bijective
proof end;
end;

:: deftheorem Def19 defines are_isomorphic GROUP_9:def 19 :
for O being set
for G, H being GroupWithOperators of O holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

Lm12: for O being set
for G, H being GroupWithOperators of O st G,H are_isomorphic holds
H,G are_isomorphic

proof end;

definition
let O be set ;
let G, H be GroupWithOperators of O;
:: original: are_isomorphic
redefine pred G,H are_isomorphic ;
symmetry
for G, H being GroupWithOperators of O st (O,b1,b2) holds
(O,b2,b1)
by Lm12;
end;

definition
let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func nat_hom N -> Homomorphism of G,(G ./. N) means :Def20: :: GROUP_9:def 20
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = nat_hom H;
existence
ex b1 being Homomorphism of G,(G ./. N) st
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = nat_hom H
proof end;
uniqueness
for b1, b2 being Homomorphism of G,(G ./. N) st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b1 = nat_hom H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b2 = nat_hom H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines nat_hom GROUP_9:def 20 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b4 being Homomorphism of G,(G ./. N) holds
( b4 = nat_hom N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b4 = nat_hom H );

Lm13: for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

proof end;

Lm14: for O being set
for G, H being GroupWithOperators of O
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "

proof end;

Lm15: for O being set
for G being GroupWithOperators of O
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) & ( for o being Element of O
for g being Element of G st g in A holds
(G ^ o) . g in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A

proof end;

definition
let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
func Ker g -> strict StableSubgroup of G means :Def21: :: GROUP_9:def 21
the carrier of it = { a where a is Element of G : g . a = 1_ H } ;
existence
ex b1 being strict StableSubgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H }
proof end;
uniqueness
for b1, b2 being strict StableSubgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } & the carrier of b2 = { a where a is Element of G : g . a = 1_ H } holds
b1 = b2
by Lm5;
end;

:: deftheorem Def21 defines Ker GROUP_9:def 21 :
for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H
for b5 being strict StableSubgroup of G holds
( b5 = Ker g iff the carrier of b5 = { a where a is Element of G : g . a = 1_ H } );

registration
let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
cluster Ker g -> strict normal ;
correctness
coherence
Ker g is normal
;
proof end;
end;

Lm16: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G

proof end;

Lm17: for O being set
for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9

proof end;

definition
let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
func Image g -> strict StableSubgroup of H means :Def22: :: GROUP_9:def 22
the carrier of it = g .: the carrier of G;
existence
ex b1 being strict StableSubgroup of H st the carrier of b1 = g .: the carrier of G
proof end;
uniqueness
for b1, b2 being strict StableSubgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds
b1 = b2
by Lm5;
end;

:: deftheorem Def22 defines Image GROUP_9:def 22 :
for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H
for b5 being strict StableSubgroup of H holds
( b5 = Image g iff the carrier of b5 = g .: the carrier of G );

definition
let O be set ;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
func carr H -> Subset of G equals :: GROUP_9:def 23
the carrier of H;
coherence
the carrier of H is Subset of G
proof end;
end;

:: deftheorem defines carr GROUP_9:def 23 :
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds carr H = the carrier of H;

definition
let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 * H2 -> Subset of G equals :: GROUP_9:def 24
(carr H1) * (carr H2);
coherence
(carr H1) * (carr H2) is Subset of G
;
end;

:: deftheorem defines * GROUP_9:def 24 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 * H2 = (carr H1) * (carr H2);

Lm18: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds 1_ G in H

proof end;

Lm19: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g1, g2 being Element of G st g1 in H & g2 in H holds
g1 * g2 in H

proof end;

Lm20: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
g " in H

proof end;

definition
let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 /\ H2 -> strict StableSubgroup of G means :Def25: :: GROUP_9:def 25
the carrier of it = (carr H1) /\ (carr H2);
existence
ex b1 being strict StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2)
proof end;
uniqueness
for b1, b2 being strict StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds
b1 = b2
by Lm5;
commutativity
for b1 being strict StableSubgroup of G
for H1, H2 being StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) holds
the carrier of b1 = (carr H2) /\ (carr H1)
;
end;

:: deftheorem Def25 defines /\ GROUP_9:def 25 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for b5 being strict StableSubgroup of G holds
( b5 = H1 /\ H2 iff the carrier of b5 = (carr H1) /\ (carr H2) );

Lm21: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2

proof end;

:: like GROUP_4:def 5
definition
let O be set ;
let G be GroupWithOperators of O;
let A be Subset of G;
func the_stable_subgroup_of A -> strict StableSubgroup of G means :Def26: :: GROUP_9:def 26
( A c= the carrier of it & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
it is StableSubgroup of H ) );
existence
ex b1 being strict StableSubgroup of G st
( A c= the carrier of b1 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
b1 is StableSubgroup of H ) )
proof end;
uniqueness
for b1, b2 being strict StableSubgroup of G st A c= the carrier of b1 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
b1 is StableSubgroup of H ) & A c= the carrier of b2 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
b2 is StableSubgroup of H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines the_stable_subgroup_of GROUP_9:def 26 :
for O being set
for G being GroupWithOperators of O
for A being Subset of G
for b4 being strict StableSubgroup of G holds
( b4 = the_stable_subgroup_of A iff ( A c= the carrier of b4 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
b4 is StableSubgroup of H ) ) );

definition
let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 "\/" H2 -> strict StableSubgroup of G equals :: GROUP_9:def 27
the_stable_subgroup_of ((carr H1) \/ (carr H2));
correctness
coherence
the_stable_subgroup_of ((carr H1) \/ (carr H2)) is strict StableSubgroup of G
;
;
end;

:: deftheorem defines "\/" GROUP_9:def 27 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of ((carr H1) \/ (carr H2));

begin

:: GROUP_2:49
theorem Th1: :: GROUP_9:1
for O, x being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G st x in H1 holds
x in G
proof end;

:: GROUP_2:51
theorem Th2: :: GROUP_9:2
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for h1 being Element of H1 holds h1 is Element of G
proof end;

:: GROUP_2:52
theorem Th3: :: GROUP_9:3
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G
for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
proof end;

:: GROUP_2:53
theorem Th4: :: GROUP_9:4
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G = 1_ H1
proof end;

:: GROUP_2:55
theorem :: GROUP_9:5
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G in H1 by Lm18;

:: GROUP_2:57
theorem Th6: :: GROUP_9:6
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "
proof end;

:: GROUP_2:59
theorem :: GROUP_9:7
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G st g1 in H1 & g2 in H1 holds
g1 * g2 in H1 by Lm19;

:: GROUP_2:60
theorem :: GROUP_9:8
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
g1 " in H1 by Lm20;

:: GROUP_2:61
theorem :: GROUP_9:9
for O being set
for G being GroupWithOperators of O
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g1 being Element of G st g1 in A holds
g1 " in A ) & ( for o being Element of O
for g1 being Element of G st g1 in A holds
(G ^ o) . g1 in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A by Lm15;

:: GROUP_2:63
theorem Th10: :: GROUP_9:10
for O being set
for G being GroupWithOperators of O holds G is StableSubgroup of G
proof end;

:: GROUP_2:65
theorem Th11: :: GROUP_9:11
for O being set
for G1, G2, G3 being GroupWithOperators of O st G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 holds
G1 is StableSubgroup of G3
proof end;

:: GROUP_2:66
theorem :: GROUP_9:12
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2 by Lm21;

:: GROUP_2:67
theorem Th13: :: GROUP_9:13
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is StableSubgroup of H2
proof end;

:: GROUP_2:68
theorem :: GROUP_9:14
for O being set
for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2 by Lm5;

:: GROUP_2:75
theorem Th15: :: GROUP_9:15
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G = (1). H1
proof end;

:: GROUP_2:77
theorem Th16: :: GROUP_9:16
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1
proof end;

:: GROUP_2:93
theorem Th17: :: GROUP_9:17
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
proof end;

:: GROUP_2:97
theorem Th18: :: GROUP_9:18
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( ( for H being StableSubgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
proof end;

:: GROUP_2:100
theorem Th19: :: GROUP_9:19
for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds H /\ H = H
proof end;

:: GROUP_2:102
theorem Th20: :: GROUP_9:20
for O being set
for G being GroupWithOperators of O
for H1, H2, H3 being StableSubgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
proof end;

Lm22: for O being set
for G being GroupWithOperators of O
for H2 being StableSubgroup of G
for H1 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

proof end;

:: GROUP_2:103
theorem Th21: :: GROUP_9:21
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )
proof end;

:: GROUP_2:167
theorem Th22: :: GROUP_9:22
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds union (Cosets N) = the carrier of G
proof end;

:: GROUP_3:149
theorem Th23: :: GROUP_9:23
for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2)
proof end;

Lm23: for F1 being FinSequence
for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )

proof end;

Lm24: for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

proof end;

:: GROUP_4:37
theorem Th24: :: GROUP_9:24
for O being set
for G being GroupWithOperators of O
for A being Subset of G
for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )
proof end;

Lm25: for O being set
for G being GroupWithOperators of O
for A being Subset of G st A is empty holds
the_stable_subgroup_of A = (1). G

proof end;

Lm26: for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o

proof end;

Lm27: for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A))

proof end;

Lm28: for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

proof end;

Lm29: for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))

proof end;

Lm30: for O, E being set
for F being FinSequence of O
for Y being Subset of E
for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y

proof end;

Lm31: for O being set
for E being non empty set
for A being Action of O,E
for X being Subset of E
for a being Element of E st not X is empty holds
( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

proof end;

:: GROUP_4:40
theorem Th25: :: GROUP_9:25
for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H
proof end;

:: GROUP_4:41
theorem Th26: :: GROUP_9:26
for O being set
for G being GroupWithOperators of O
for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
proof end;

scheme :: GROUP_9:sch 1
MeetSbgWOpEx{ F1() -> set , F2() -> GroupWithOperators of F1(), P1[ set ] } :
ex H being strict StableSubgroup of F2() st the carrier of H = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
provided
A1: ex H being strict StableSubgroup of F2() st P1[H]
proof end;

:: GROUP_4:43
theorem Th27: :: GROUP_9:27
for O being set
for G being GroupWithOperators of O
for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
proof end;

Lm32: for O being set
for G being GroupWithOperators of O
for B, A being Subset of G st B = the carrier of (gr A) holds
the_stable_subgroup_of A = the_stable_subgroup_of B

proof end;

:: GROUP_4:64
theorem Th28: :: GROUP_9:28
for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1
proof end;

:: GROUP_4:68
theorem Th29: :: GROUP_9:29
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)
proof end;

:: GROUP_4:69
theorem Th30: :: GROUP_9:30
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
proof end;

:: GROUP_4:71
theorem Th31: :: GROUP_9:31
for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2
proof end;

:: GROUP_4:72
theorem Th32: :: GROUP_9:32
for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 "\/" N2 is normal StableSubgroup of G
proof end;

:: GROUP_4:76
theorem Th33: :: GROUP_9:33
for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
proof end;

:: GROUP_4:77
theorem Th34: :: GROUP_9:34
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )
proof end;

Lm33: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2

proof end;

:: GROUP_4:78
theorem Th35: :: GROUP_9:35
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )
proof end;

:: GROUP_4:79
theorem Th36: :: GROUP_9:36
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 "\/" H2 = H2 )
proof end;

:: GROUP_4:81
theorem Th37: :: GROUP_9:37
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for H3 being strict StableSubgroup of G st H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 holds
H1 "\/" H2 is StableSubgroup of H3
proof end;

:: GROUP_4:82
theorem Th38: :: GROUP_9:38
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds
H1 "\/" H3 is StableSubgroup of H2 "\/" H3
proof end;

:: GROUP_6:3
theorem Th39: :: GROUP_9:39
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for X, Y being StableSubgroup of H1
for X9, Y9 being StableSubgroup of G st X = X9 & Y = Y9 holds
X9 /\ Y9 = X /\ Y
proof end;

:: GROUP_6:9
theorem Th40: :: GROUP_9:40
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds
N is normal StableSubgroup of H1
proof end;

Lm34: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1

proof end;

:: GROUP_6:10
theorem Th41: :: GROUP_9:41
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
proof end;

:: GROUP_6:13
theorem Th42: :: GROUP_9:42
for O being set
for G being strict GroupWithOperators of O st G is trivial holds
(1). G = G
proof end;

Lm35: for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds
( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

proof end;

:: GROUP_6:29
theorem Th43: :: GROUP_9:43
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N
proof end;

:: GROUP_6:35
theorem Th44: :: GROUP_9:44
for O being set
for G being GroupWithOperators of O
for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M
proof end;

:: GROUP_6:40
theorem :: GROUP_9:45
for O being set
for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds h . (1_ G) = 1_ H by Lm13;

:: GROUP_6:41
theorem :: GROUP_9:46
for O being set
for G, H being GroupWithOperators of O
for g1 being Element of G
for h being Homomorphism of G,H holds h . (g1 ") = (h . g1) " by Lm14;

:: GROUP_6:50
theorem Th47: :: GROUP_9:47
for O being set
for G, H being GroupWithOperators of O
for g1 being Element of G
for h being Homomorphism of G,H holds
( g1 in Ker h iff h . g1 = 1_ H )
proof end;

:: GROUP_6:52
theorem Th48: :: GROUP_9:48
for O being set
for G being GroupWithOperators of O
for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N
proof end;

:: GROUP_6:53
theorem Th49: :: GROUP_9:49
for O being set
for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds rng h = the carrier of (Image h)
proof end;

:: GROUP_6:57
theorem Th50: :: GROUP_9:50
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds Image (nat_hom N) = G ./. N
proof end;

:: GROUP_6:67
theorem Th51: :: GROUP_9:51
for O being set
for G being GroupWithOperators of O
for H being strict GroupWithOperators of O
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
proof end;

:: GROUP_6:68
theorem Th52: :: GROUP_9:52
for O being set
for G being GroupWithOperators of O
for H being strict GroupWithOperators of O
for h being Homomorphism of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c
proof end;

:: GROUP_6:69
theorem Th53: :: GROUP_9:53
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds nat_hom N is onto
proof end;

:: GROUP_6:75
theorem Th54: :: GROUP_9:54
for O being set
for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective
proof end;

:: GROUP_6:78
theorem Th55: :: GROUP_9:55
for O being set
for G, H, I being GroupWithOperators of O st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic
proof end;

:: GROUP_6:82
theorem Th56: :: GROUP_9:56
for O being set
for G being strict GroupWithOperators of O holds G,G ./. ((1). G) are_isomorphic
proof end;

:: GROUP_6:83
theorem Th57: :: GROUP_9:57
for O being set
for G being strict GroupWithOperators of O holds G ./. ((Omega). G) is trivial
proof end;

:: GROUP_6:87
theorem Th58: :: GROUP_9:58
for O being set
for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is trivial holds
H is trivial
proof end;

:: GROUP_6:90
theorem Th59: :: GROUP_9:59
for O being set
for H, G being GroupWithOperators of O
for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic
proof end;

:: GRSOLV_1:1
theorem Th60: :: GROUP_9:60
for O being set
for G being GroupWithOperators of O
for H, F1, F2 being strict StableSubgroup of G st F1 is normal StableSubgroup of F2 holds
H /\ F1 is normal StableSubgroup of H /\ F2
proof end;

begin

theorem :: GROUP_9:61
for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A by Lm1;

theorem :: GROUP_9:62
for O, E being set holds [:O,{(id E)}:] is Action of O,E by Lm2;

theorem :: GROUP_9:63
for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o by Lm26;

theorem :: GROUP_9:64
for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by Lm29;

theorem :: GROUP_9:65
for O, E being set
for A being Action of O,E
for F being FinSequence of O
for Y being Subset of E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y by Lm30;

theorem :: GROUP_9:66
for O being set
for E being non empty set
for A being Action of O,E
for X being Subset of E
for a being Element of E st not X is empty holds
( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) by Lm31;

theorem :: GROUP_9:67
for O being set
for G being strict Group ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #)
proof end;

theorem :: GROUP_9:68
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds multMagma(# the carrier of H1, the multF of H1 #) is strict Subgroup of G by Lm16;

theorem :: GROUP_9:69
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G by Lm7;

theorem :: GROUP_9:70
for O being set
for o being Element of O
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
(G ^ o) . g1 in H1 by Lm10;

theorem :: GROUP_9:71
for O being set
for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9 by Lm17;

theorem :: GROUP_9:72
for O being set
for G being GroupWithOperators of O
for B being Subset of G st B is empty holds
the_stable_subgroup_of B = (1). G by Lm25;

theorem :: GROUP_9:73
for O being set
for G being GroupWithOperators of O
for B, C being Subset of G st B = the carrier of (gr C) holds
the_stable_subgroup_of C = the_stable_subgroup_of B by Lm32;

theorem :: GROUP_9:74
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds
( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) by Lm35;

theorem Th75: :: GROUP_9:75
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)
proof end;

theorem Th76: :: GROUP_9:76
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)
proof end;

theorem Th77: :: GROUP_9:77
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial
proof end;

:: ALG I.4.6 Proposition 7(a)
theorem Th78: :: GROUP_9:78
for O being set
for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for H9 being strict StableSubgroup of H
for f being Homomorphism of G,H st N = Ker f holds
ex G9 being strict StableSubgroup of G st
( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )
proof end;

:: ALG I.4.6 Proposition 7(b)
theorem Th79: :: GROUP_9:79
for O being set
for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
proof end;

theorem Th80: :: GROUP_9:80
for O being set
for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of G = (nat_hom N) " the carrier of H holds
H = (Omega). (G ./. N)
proof end;

theorem Th81: :: GROUP_9:81
for O being set
for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom N) " the carrier of H holds
H = (1). (G ./. N)
proof end;

theorem Th82: :: GROUP_9:82
for O being set
for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is simple holds
H is simple
proof end;

theorem Th83: :: GROUP_9:83
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for FG being FinSequence of the carrier of G
for FH being FinSequence of the carrier of H
for I being FinSequence of INT st FG = FH & len FG = len I holds
Product (FG |^ I) = Product (FH |^ I)
proof end;

theorem Th84: :: GROUP_9:84
for O, E1, E2 being set
for A1 being Action of O,E1
for A2 being Action of O,E2
for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1
proof end;

theorem Th85: :: GROUP_9:85
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2
proof end;

theorem Th86: :: GROUP_9:86
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 "\/" N29 = N1 "\/" N2
proof end;

theorem Th87: :: GROUP_9:87
for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of G st N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds
N1 "\/" N2 is normal StableSubgroup of H1
proof end;

theorem Th88: :: GROUP_9:88
for O being set
for G, H, I being GroupWithOperators of O
for f being Homomorphism of G,H
for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
proof end;

theorem Th89: :: GROUP_9:89
for O being set
for G, H being GroupWithOperators of O
for G9 being StableSubgroup of G
for H9 being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9
proof end;

:: ALG I.4.6 Corollary 2
theorem Th90: :: GROUP_9:90
for O being set
for G, H being strict GroupWithOperators of O
for N, L, G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
proof end;

begin

theorem Th91: :: GROUP_9:91
for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G
for JH being normal StableSubgroup of H9 "\/" (H /\ K)
for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds
(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic
proof end;

theorem Th92: :: GROUP_9:92
for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)
proof end;

:: WP: Zassenhaus Lemma
theorem Th93: :: GROUP_9:93
for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G
for JH being normal StableSubgroup of H9 "\/" (H /\ K)
for JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
(H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic
proof end;

begin

:: ALG I.4.7 Definition 9
definition
let O be set ;
let G be GroupWithOperators of O;
let IT be FinSequence of the_stable_subgroups_of G;
attr IT is composition_series means :Def28: :: GROUP_9:def 28
( IT . 1 = (Omega). G & IT . (len IT) = (1). G & ( for i being Nat st i in dom IT & i + 1 in dom IT holds
for H1, H2 being StableSubgroup of G st H1 = IT . i & H2 = IT . (i + 1) holds
H2 is normal StableSubgroup of H1 ) );
end;

:: deftheorem Def28 defines composition_series GROUP_9:def 28 :
for O being set
for G being GroupWithOperators of O
for IT being FinSequence of the_stable_subgroups_of G holds
( IT is composition_series iff ( IT . 1 = (Omega). G & IT . (len IT) = (1). G & ( for i being Nat st i in dom IT & i + 1 in dom IT holds
for H1, H2 being StableSubgroup of G st H1 = IT . i & H2 = IT . (i + 1) holds
H2 is normal StableSubgroup of H1 ) ) );

registration
let O be set ;
let G be GroupWithOperators of O;
cluster Relation-like NAT -defined the_stable_subgroups_of G -valued Function-like finite FinSequence-like FinSubsequence-like composition_series for FinSequence of the_stable_subgroups_of G;
existence
ex b1 being FinSequence of the_stable_subgroups_of G st b1 is composition_series
proof end;
end;

definition
let O be set ;
let G be GroupWithOperators of O;
mode CompositionSeries of G is composition_series FinSequence of the_stable_subgroups_of G;
end;

:: ALG I.4.7 Definition 9
definition
let O be set ;
let G be GroupWithOperators of O;
let s1, s2 be CompositionSeries of G;
pred s1 is_finer_than s2 means :Def29: :: GROUP_9:def 29
ex x being set st
( x c= dom s1 & s2 = s1 * (Sgm x) );
reflexivity
for s1 being CompositionSeries of G ex x being set st
( x c= dom s1 & s1 = s1 * (Sgm x) )
proof end;
end;

:: deftheorem Def29 defines is_finer_than GROUP_9:def 29 :
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G holds
( s1 is_finer_than s2 iff ex x being set st
( x c= dom s1 & s2 = s1 * (Sgm x) ) );

definition
let O be set ;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is strictly_decreasing means :Def30: :: GROUP_9:def 30
for i being Nat st i in dom IT & i + 1 in dom IT holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = IT . i & N = IT . (i + 1) holds
not H ./. N is trivial ;
end;

:: deftheorem Def30 defines strictly_decreasing GROUP_9:def 30 :
for O being set
for G being GroupWithOperators of O
for IT being CompositionSeries of G holds
( IT is strictly_decreasing iff for i being Nat st i in dom IT & i + 1 in dom IT holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = IT . i & N = IT . (i + 1) holds
not H ./. N is trivial );

:: ALG I.4.7 Definition 10
definition
let O be set ;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is jordan_holder means :Def31: :: GROUP_9:def 31
( IT is strictly_decreasing & ( for s being CompositionSeries of G holds
( not s <> IT or not s is strictly_decreasing or not s is_finer_than IT ) ) );
end;

:: deftheorem Def31 defines jordan_holder GROUP_9:def 31 :
for O being set
for G being GroupWithOperators of O
for IT being CompositionSeries of G holds
( IT is jordan_holder iff ( IT is strictly_decreasing & ( for s being CompositionSeries of G holds
( not s <> IT or not s is strictly_decreasing or not s is_finer_than IT ) ) ) );

:: ALG I.4.7 Definition 9
definition
let O be set ;
let G1, G2 be GroupWithOperators of O;
let s1 be CompositionSeries of G1;
let s2 be CompositionSeries of G2;
pred s1 is_equivalent_with s2 means :Def32: :: GROUP_9:def 32
( len s1 = len s2 & ( for n being Nat st n + 1 = len s1 holds
ex p being Permutation of (Seg n) st
for H1 being StableSubgroup of G1
for H2 being StableSubgroup of G2
for N1 being normal StableSubgroup of H1
for N2 being normal StableSubgroup of H2
for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic ) );
end;

:: deftheorem Def32 defines is_equivalent_with GROUP_9:def 32 :
for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 holds
( s1 is_equivalent_with s2 iff ( len s1 = len s2 & ( for n being Nat st n + 1 = len s1 holds
ex p being Permutation of (Seg n) st
for H1 being StableSubgroup of G1
for H2 being StableSubgroup of G2
for N1 being normal StableSubgroup of H1
for N2 being normal StableSubgroup of H2
for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic ) ) );

:: ALG I.4.7 Definition 9
definition
let O be set ;
let G be GroupWithOperators of O;
let s be CompositionSeries of G;
func the_series_of_quotients_of s -> FinSequence means :Def33: :: GROUP_9:def 33
( len s = (len it) + 1 & ( for i being Nat st i in dom it holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
it . i = H ./. N ) ) if len s > 1
otherwise it = {} ;
existence
( ( len s > 1 implies ex b1 being FinSequence st
( len s = (len b1) + 1 & ( for i being Nat st i in dom b1 holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b1 . i = H ./. N ) ) ) & ( not len s > 1 implies ex b1 being FinSequence st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being FinSequence holds
( ( len s > 1 & len s = (len b1) + 1 & ( for i being Nat st i in dom b1 holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b1 . i = H ./. N ) & len s = (len b2) + 1 & ( for i being Nat st i in dom b2 holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b2 . i = H ./. N ) implies b1 = b2 ) & ( not len s > 1 & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being FinSequence holds verum
;
end;

:: deftheorem Def33 defines the_series_of_quotients_of GROUP_9:def 33 :
for O being set
for G being GroupWithOperators of O
for s being CompositionSeries of G
for b4 being FinSequence holds
( ( len s > 1 implies ( b4 = the_series_of_quotients_of s iff ( len s = (len b4) + 1 & ( for i being Nat st i in dom b4 holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
b4 . i = H ./. N ) ) ) ) & ( not len s > 1 implies ( b4 = the_series_of_quotients_of s iff b4 = {} ) ) );

definition
let O be set ;
let f1, f2 be FinSequence;
let p be Permutation of (dom f1);
pred f1,f2 are_equivalent_under p,O means :Def34: :: GROUP_9:def 34
( len f1 = len f2 & ( for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom f1 & j = (p ") . i & H1 = f1 . i & H2 = f2 . j holds
H1,H2 are_isomorphic ) );
end;

:: deftheorem Def34 defines are_equivalent_under GROUP_9:def 34 :
for O being set
for f1, f2 being FinSequence
for p being Permutation of (dom f1) holds
( f1,f2 are_equivalent_under p,O iff ( len f1 = len f2 & ( for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom f1 & j = (p ") . i & H1 = f1 . i & H2 = f2 . j holds
H1,H2 are_isomorphic ) ) );

theorem Th94: :: GROUP_9:94
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for fs being FinSequence of the_stable_subgroups_of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series
proof end;

theorem Th95: :: GROUP_9:95
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds
ex n being Nat st len s1 = (len s2) + n
proof end;

theorem Th96: :: GROUP_9:96
for O being set
for G being GroupWithOperators of O
for s2, s1 being CompositionSeries of G st len s2 = len s1 & s2 is_finer_than s1 holds
s1 = s2
proof end;

theorem Th97: :: GROUP_9:97
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st not s1 is empty & s2 is_finer_than s1 holds
not s2 is empty
proof end;

theorem Th98: :: GROUP_9:98
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder holds
s1 = s2
proof end;

Lm36: for P, R being Relation holds
( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) )

proof end;

Lm37: for X being set
for P, R being Relation holds P * (R | X) = (X |` P) * R

proof end;

Lm38: for n being Nat
for X being set
for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds
Sgm (f .: X) = f * (Sgm X)

proof end;

Lm39: for y being set
for n, i being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

proof end;

theorem Th99: :: GROUP_9:99
for O being set
for G being GroupWithOperators of O
for s1, s19, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds
s19 is_finer_than s2
proof end;

theorem Th100: :: GROUP_9:100
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
proof end;

theorem Th101: :: GROUP_9:101
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for s1 being CompositionSeries of G
for i, j being Nat st i in dom s1 & j in dom s1 & i <= j & H1 = s1 . i & H2 = s1 . j holds
H2 is StableSubgroup of H1
proof end;

theorem Th102: :: GROUP_9:102
for O being set
for G being GroupWithOperators of O
for y being set
for s1 being CompositionSeries of G st y in rng (the_series_of_quotients_of s1) holds
y is strict GroupWithOperators of O
proof end;

theorem Th103: :: GROUP_9:103
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for i being Nat st i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds
H is trivial ) holds
( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )
proof end;

theorem Th104: :: GROUP_9:104
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)
proof end;

theorem :: GROUP_9:105
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for f1 being FinSequence
for i being Nat st f1 = the_series_of_quotients_of s1 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) holds
( Del (s1,i) is CompositionSeries of G & ( for s2 being CompositionSeries of G st s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del (f1,i) ) )
proof end;

theorem Th106: :: GROUP_9:106
for O being set
for f1, f2 being FinSequence
for i, j being Nat st i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) holds
ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O
proof end;

theorem Th107: :: GROUP_9:107
for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2
proof end;

theorem Th108: :: GROUP_9:108
for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds
( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
proof end;

theorem Th109: :: GROUP_9:109
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds
ex i being Nat st
( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds
H is trivial ) )
proof end;

Lm40: for k, m being Element of NAT holds
( k < m iff k <= m - 1 )

proof end;

Lm41: for a being Element of NAT
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )

proof end;

Lm42: for a being Element of NAT
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2

proof end;

Lm43: for a being Element of NAT
for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )

proof end;

Lm44: for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))

proof end;

:: ALG I.4.7 Proposition 9
theorem Th110: :: GROUP_9:110
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G st len s1 > 1 holds
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )
proof end;

theorem Th111: :: GROUP_9:111
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for i being Nat st 1 <= i & i <= (len s1) - 1 holds
( s1 . i is strict StableSubgroup of G & s1 . (i + 1) is strict StableSubgroup of G )
proof end;

theorem Th112: :: GROUP_9:112
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for s1 being CompositionSeries of G
for i being Nat st 1 <= i & i <= (len s1) - 1 & H1 = s1 . i & H2 = s1 . (i + 1) holds
H2 is normal StableSubgroup of H1
proof end;

theorem Th113: :: GROUP_9:113
for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G holds s1 is_equivalent_with s1
proof end;

theorem Th114: :: GROUP_9:114
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds
s2 is_finer_than s1
proof end;

theorem Th115: :: GROUP_9:115
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_equivalent_with s2 & s1 is jordan_holder holds
s2 is jordan_holder
proof end;

Lm45: for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )

proof end;

Lm46: for O being set
for G being GroupWithOperators of O
for i1, j1, i2, j2 being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )

proof end;

Lm47: for O being set
for G being GroupWithOperators of O
for k being integer number
for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )

proof end;

begin

definition
let O be set ;
let G be GroupWithOperators of O;
let s1, s2 be CompositionSeries of G;
assume that
A1: len s1 > 1 and
A2: len s2 > 1 ;
func the_schreier_series_of (s1,s2) -> CompositionSeries of G means :Def35: :: GROUP_9:def 35
for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies it . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies it . k = (1). G ) & len it = (((len s1) - 1) * ((len s2) - 1)) + 1 );
existence
ex b1 being CompositionSeries of G st
for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((len s1) - 1) * ((len s2) - 1)) + 1 )
proof end;
uniqueness
for b1, b2 being CompositionSeries of G st ( for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) & ( for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies b2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b2 . k = (1). G ) & len b2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def35 defines the_schreier_series_of GROUP_9:def 35 :
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
for b5 being CompositionSeries of G holds
( b5 = the_schreier_series_of (s1,s2) iff for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies b5 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b5 . k = (1). G ) & len b5 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) );

theorem Th116: :: GROUP_9:116
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1
proof end;

theorem Th117: :: GROUP_9:117
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1)
proof end;

:: ALG I.4.7 Theorem 5
:: WP: Schreier Refinement Theorem
theorem Th118: :: GROUP_9:118
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )
proof end;

begin

:: ALG I.4.7 Theorem 6
:: WP: Jordan-H\"older Theorem
theorem :: GROUP_9:119
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds
s1 is_equivalent_with s2
proof end;

begin

theorem :: GROUP_9:120
for P, R being Relation holds
( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) ) by Lm36;

theorem :: GROUP_9:121
for X being set
for P, R being Relation holds P * (R | X) = (X |` P) * R by Lm37;

theorem :: GROUP_9:122
for n being Nat
for X being set
for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds
Sgm (f .: X) = f * (Sgm X) by Lm38;

theorem :: GROUP_9:123
for y being set
for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) by Lm39;

theorem :: GROUP_9:124
for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1)) by Lm44;

theorem :: GROUP_9:125
for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I) by Lm24;