let O be set ; :: thesis: 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 )
let G be GroupWithOperators of O; :: thesis: 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 )
let s1 be CompositionSeries of G; :: thesis: 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 )
let i be Nat; :: thesis: ( 1 <= i & i <= (len s1) - 1 implies ( s1 . i is strict StableSubgroup of G & s1 . (i + 1) is strict StableSubgroup of G ) )
assume that
A1: 1 <= i and
A2: i <= (len s1) - 1 ; :: thesis: ( s1 . i is strict StableSubgroup of G & s1 . (i + 1) is strict StableSubgroup of G )
A3: 0 + i <= 1 + i by XREAL_1:6;
A4: i + 1 <= ((len s1) - 1) + 1 by A2, XREAL_1:6;
then i <= len s1 by A3, XXREAL_0:2;
then i in Seg (len s1) by A1;
then i in dom s1 by FINSEQ_1:def 3;
then s1 . i is Element of the_stable_subgroups_of G by FINSEQ_2:11;
hence s1 . i is strict StableSubgroup of G by Def11; :: thesis: s1 . (i + 1) is strict StableSubgroup of G
1 <= i + 1 by A1, A3, XXREAL_0:2;
then i + 1 in Seg (len s1) by A4;
then i + 1 in dom s1 by FINSEQ_1:def 3;
then s1 . (i + 1) is Element of the_stable_subgroups_of G by FINSEQ_2:11;
hence s1 . (i + 1) is strict StableSubgroup of G by Def11; :: thesis: verum