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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[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: S1[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 S1[n + 1] ; :: thesis: verum
end;
suppose not i + n in dom s1 ; :: thesis: S1[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: S1[n + 1]
then n = 0 by NAT_1:13;
hence S1[n + 1] by A1, A4, Def28; :: thesis: verum
end;
suppose A12: i + n > len s1 ; :: thesis: S1[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 S1[n + 1] by FINSEQ_1:def 3; :: thesis: verum
end;
end;
end;
end;
end;
A14: S1[ 0 ] by A4, Th10;
A15: for n being Nat holds S1[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