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, 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
let G be GroupWithOperators of O; :: thesis: 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
let H1, H2 be StableSubgroup of G; :: thesis: 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
let s1 be CompositionSeries of G; :: thesis: 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
let i, j be Nat; :: thesis: ( i in dom s1 & j in dom s1 & i <= j & H1 = s1 . i & H2 = s1 . j implies H2 is StableSubgroup of H1 )
assume that
A1: i in dom s1 and
A2: j in dom s1 ; :: thesis: ( not i <= j or not H1 = s1 . i or not H2 = s1 . j or H2 is StableSubgroup of H1 )
defpred S₁[ Nat] means for n being Nat
for H2 being StableSubgroup of G st i + $1 in dom s1 & H2 = s1 . (i + $1) holds
H2 is StableSubgroup of H1;
assume A3: i <= j ; :: thesis: ( not H1 = s1 . i or not H2 = s1 . j or H2 is StableSubgroup of H1 )
assume that
A4: H1 = s1 . i and
A5: H2 = s1 . j ; :: thesis: H2 is StableSubgroup of H1
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
set H2 = s1 . (i + n);

per cases ( i + n in dom s1 or not i + n in dom s1 ) ;

suppose A8: i + n in dom s1 ; :: thesis: S₁[n + 1]

then reconsider H2 = s1 . (i + n) as Element of the_stable_subgroups_of G by FINSEQ_2:11;
reconsider H2 = H2 as StableSubgroup of G by Def11;
A9: H2 is StableSubgroup of H1 by A7, A8;

now :: thesis: for k being Element of NAT
for H3 being StableSubgroup of G st i + (n + 1) in dom s1 & H3 = s1 . (i + (n + 1)) holds
H3 is StableSubgroup of H1

let k be Element of NAT ; :: thesis: for H3 being StableSubgroup of G st i + (n + 1) in dom s1 & H3 = s1 . (i + (n + 1)) holds
H3 is StableSubgroup of H1
let H3 be StableSubgroup of G; :: thesis: ( i + (n + 1) in dom s1 & H3 = s1 . (i + (n + 1)) implies H3 is StableSubgroup of H1 )
assume i + (n + 1) in dom s1 ; :: thesis: ( H3 = s1 . (i + (n + 1)) implies H3 is StableSubgroup of H1 )
then A10: (i + n) + 1 in dom s1 ;
assume H3 = s1 . (i + (n + 1)) ; :: thesis: H3 is StableSubgroup of H1
then H3 is StableSubgroup of H2 by A8, A10, Def28;
hence H3 is StableSubgroup of H1 by A9, Th11; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

suppose not i + n in dom s1 ; :: thesis: S₁[n + 1]

then A11: not i + n in Seg (len s1) by FINSEQ_1:def 3;

per cases ( i + n < 0 + 1 or i + n > len s1 ) by A11;

suppose i + n < 0 + 1 ; :: thesis: S₁[n + 1]

then n = 0 by NAT_1:13;
hence S₁[n + 1] by A1, A4, Def28; :: thesis: verum

end;

suppose A12: i + n > len s1 ; :: thesis: S₁[n + 1]

A13: 1 + (len s1) > 0 + (len s1) by XREAL_1:6;
(i + n) + 1 > (len s1) + 1 by A12, XREAL_1:6;
then (i + n) + 1 > len s1 by A13, XXREAL_0:2;
then not (i + n) + 1 in Seg (len s1) by FINSEQ_1:1;
hence S₁[n + 1] by FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

end;

end;

A14: S₁[ 0 ] by A4, Th10;
A15: for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A6);
set n = j - i;
i - i <= j - i by A3, XREAL_1:9;
then reconsider n = j - i as Element of NAT by INT_1:3;
reconsider n = n as Nat ;
j = i + n ;
hence H2 is StableSubgroup of H1 by A2, A5, A15; :: thesis: verum