let O be set ; :: thesis: 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

let G be GroupWithOperators of O; :: thesis: 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

let H1, H2 be StableSubgroup of G; :: thesis: 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

let s1 be CompositionSeries of G; :: thesis: 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

let i be Nat; :: thesis: ( 1 <= i & i <= (len s1) - 1 & H1 = s1 . i & H2 = s1 . (i + 1) implies H2 is normal StableSubgroup of H1 )

assume that

A1: 1 <= i and

A2: i <= (len s1) - 1 ; :: thesis: ( not H1 = s1 . i or not H2 = s1 . (i + 1) or H2 is normal StableSubgroup of H1 )

A3: i + 1 <= ((len s1) - 1) + 1 by A2, XREAL_1:6;

A4: 0 + i <= 1 + i by XREAL_1:6;

then 1 <= i + 1 by A1, XXREAL_0:2;

then i + 1 in Seg (len s1) by A3;

then A5: i + 1 in dom s1 by FINSEQ_1:def 3;

i <= len s1 by A4, A3, XXREAL_0:2;

then i in Seg (len s1) by A1;

then A6: i in dom s1 by FINSEQ_1:def 3;

assume ( H1 = s1 . i & H2 = s1 . (i + 1) ) ; :: thesis: H2 is normal StableSubgroup of H1

hence H2 is normal StableSubgroup of H1 by A5, A6, Def28; :: thesis: verum

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

let G be GroupWithOperators of O; :: thesis: 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

let H1, H2 be StableSubgroup of G; :: thesis: 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

let s1 be CompositionSeries of G; :: thesis: 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

let i be Nat; :: thesis: ( 1 <= i & i <= (len s1) - 1 & H1 = s1 . i & H2 = s1 . (i + 1) implies H2 is normal StableSubgroup of H1 )

assume that

A1: 1 <= i and

A2: i <= (len s1) - 1 ; :: thesis: ( not H1 = s1 . i or not H2 = s1 . (i + 1) or H2 is normal StableSubgroup of H1 )

A3: i + 1 <= ((len s1) - 1) + 1 by A2, XREAL_1:6;

A4: 0 + i <= 1 + i by XREAL_1:6;

then 1 <= i + 1 by A1, XXREAL_0:2;

then i + 1 in Seg (len s1) by A3;

then A5: i + 1 in dom s1 by FINSEQ_1:def 3;

i <= len s1 by A4, A3, XXREAL_0:2;

then i in Seg (len s1) by A1;

then A6: i in dom s1 by FINSEQ_1:def 3;

assume ( H1 = s1 . i & H2 = s1 . (i + 1) ) ; :: thesis: H2 is normal StableSubgroup of H1

hence H2 is normal StableSubgroup of H1 by A5, A6, Def28; :: thesis: verum