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_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A4, Th10;

A15: for n being Nat holds S_{1}[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

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

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

S

proof

A14:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A7: S_{1}[n]
; :: thesis: S_{1}[n + 1]

set H2 = s1 . (i + n);

end;assume A7: S

set H2 = s1 . (i + n);

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

end;

suppose A8:
i + n in dom s1
; :: thesis: S_{1}[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;

_{1}[n + 1]
; :: thesis: verum

end;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

hence
Sfor 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;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

A15: for n being Nat holds S

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