:: 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 b₅ being CompositionSeries of G holds
( b₅ = 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 b₅ . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b₅ . k = (1). G ) & len b₅ = (((len s1) - 1) * ((len s2) - 1)) + 1 ) );