let O be set ; :: thesis: for G being GroupWithOperators of O

for s1 being CompositionSeries of G

for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G

for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let s1 be CompositionSeries of G; :: thesis: for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let fs be FinSequence of the_stable_subgroups_of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) implies fs is composition_series )

assume A1: i in dom s1 ; :: thesis: ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )

then consider k being Nat such that

A2: len s1 = k + 1 and

A3: len (Del (s1,i)) = k by FINSEQ_3:104;

assume i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )

then i + 1 in Seg (len s1) by FINSEQ_1:def 3;

then A4: i + 1 <= len s1 by FINSEQ_1:1;

assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not fs = Del (s1,i) or fs is composition_series )

assume A6: fs = Del (s1,i) ; :: thesis: fs is composition_series

A7: i in Seg (len s1) by A1, FINSEQ_1:def 3;

then A8: 1 <= i by FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then 1 + 1 <= (len fs) + 1 by A6, A4, A2, A3, XXREAL_0:2;

then A9: 1 <= len fs by XREAL_1:6;

for s1 being CompositionSeries of G

for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G

for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let s1 be CompositionSeries of G; :: thesis: for fs being FinSequence of the_stable_subgroups_of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let fs be FinSequence of the_stable_subgroups_of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds

fs is composition_series

let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) implies fs is composition_series )

assume A1: i in dom s1 ; :: thesis: ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )

then consider k being Nat such that

A2: len s1 = k + 1 and

A3: len (Del (s1,i)) = k by FINSEQ_3:104;

assume i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )

then i + 1 in Seg (len s1) by FINSEQ_1:def 3;

then A4: i + 1 <= len s1 by FINSEQ_1:1;

assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not fs = Del (s1,i) or fs is composition_series )

assume A6: fs = Del (s1,i) ; :: thesis: fs is composition_series

A7: i in Seg (len s1) by A1, FINSEQ_1:def 3;

then A8: 1 <= i by FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then 1 + 1 <= (len fs) + 1 by A6, A4, A2, A3, XXREAL_0:2;

then A9: 1 <= len fs by XREAL_1:6;

per cases
( len fs = 1 or len fs > 1 )
by A9, XXREAL_0:1;

end;

suppose A10:
len fs = 1
; :: thesis: fs is composition_series

A15: 1 <= i by A7, FINSEQ_1:1;

A16: i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;

then A17: i = 1 by A15, XXREAL_0:1;

dom s1 = Seg 2 by A6, A2, A3, A10, FINSEQ_1:def 3;

then 1 in dom s1 ;

then A18: i in dom s1 by A15, A16, XXREAL_0:1;

i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;

then A19: fs . (len fs) = s1 . (1 + 1) by A6, A2, A3, A10, A18, FINSEQ_3:111

.= (1). G by A6, A2, A3, A10, Def28 ;

s1 . 2 = (1). G by A6, A2, A3, A10, Def28;

hence fs is composition_series by A5, A10, A17, A14, A19, A11; :: thesis: verum

end;

A11: now :: thesis: for n being Nat st n in dom fs & n + 1 in dom fs holds

for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

A14:
s1 . 1 = (Omega). G
by Def28;for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

let n be Nat; :: thesis: ( n in dom fs & n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1 )

assume n in dom fs ; :: thesis: ( n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1 )

then n in Seg 1 by A10, FINSEQ_1:def 3;

then A12: n = 1 by FINSEQ_1:2, TARSKI:def 1;

assume A13: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies H2 is normal StableSubgroup of H1 )

assume that

H1 = fs . n and

H2 = fs . (n + 1) ; :: thesis: H2 is normal StableSubgroup of H1

2 in Seg 1 by A10, A12, A13, FINSEQ_1:def 3;

hence H2 is normal StableSubgroup of H1 by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;H2 is normal StableSubgroup of H1 )

assume n in dom fs ; :: thesis: ( n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1 )

then n in Seg 1 by A10, FINSEQ_1:def 3;

then A12: n = 1 by FINSEQ_1:2, TARSKI:def 1;

assume A13: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies H2 is normal StableSubgroup of H1 )

assume that

H1 = fs . n and

H2 = fs . (n + 1) ; :: thesis: H2 is normal StableSubgroup of H1

2 in Seg 1 by A10, A12, A13, FINSEQ_1:def 3;

hence H2 is normal StableSubgroup of H1 by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

A15: 1 <= i by A7, FINSEQ_1:1;

A16: i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;

then A17: i = 1 by A15, XXREAL_0:1;

dom s1 = Seg 2 by A6, A2, A3, A10, FINSEQ_1:def 3;

then 1 in dom s1 ;

then A18: i in dom s1 by A15, A16, XXREAL_0:1;

i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;

then A19: fs . (len fs) = s1 . (1 + 1) by A6, A2, A3, A10, A18, FINSEQ_3:111

.= (1). G by A6, A2, A3, A10, Def28 ;

s1 . 2 = (1). G by A6, A2, A3, A10, Def28;

hence fs is composition_series by A5, A10, A17, A14, A19, A11; :: thesis: verum

suppose A20:
len fs > 1
; :: thesis: fs is composition_series

A21:
fs . 1 = (Omega). G

then fs . (len fs) = s1 . (len s1) by A1, A6, A2, A3, FINSEQ_3:111;

then fs . (len fs) = (1). G by Def28;

hence fs is composition_series by A21, A24; :: thesis: verum

end;proof
end;

A24: now :: thesis: for n being Nat st n in dom fs & n + 1 in dom fs holds

for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

i <= len fs
by A6, A4, A2, A3, XREAL_1:6;for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

H2 is normal StableSubgroup of H1

let n be Nat; :: thesis: ( n in dom fs & n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

b_{5} is normal StableSubgroup of b_{4} )

assume that

A25: n in dom fs and

A26: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

b_{5} is normal StableSubgroup of b_{4}

A27: n in Seg (len fs) by A25, FINSEQ_1:def 3;

then A28: n <= k by A6, A3, FINSEQ_1:1;

reconsider n1 = n + 1 as Nat ;

A29: n + 1 in Seg (len fs) by A26, FINSEQ_1:def 3;

then A30: n1 <= k by A6, A3, FINSEQ_1:1;

A31: 0 + (len fs) < 1 + (len fs) by XREAL_1:6;

then A32: Seg (len fs) c= Seg (len s1) by A6, A2, A3, FINSEQ_1:5;

then n in Seg (len s1) by A27;

then A33: n in dom s1 by FINSEQ_1:def 3;

n1 in Seg (len s1) by A29, A32;

then A34: n1 in dom s1 by FINSEQ_1:def 3;

n1 <= len fs by A29, FINSEQ_1:1;

then n1 < len s1 by A6, A2, A3, A31, XXREAL_0:2;

then n1 + 1 <= k + 1 by A2, NAT_1:13;

then Seg (n1 + 1) c= Seg (len s1) by A2, FINSEQ_1:5;

then A35: Seg (n1 + 1) c= dom s1 by FINSEQ_1:def 3;

A36: n1 + 1 in Seg (n1 + 1) by FINSEQ_1:4;

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies b_{3} is normal StableSubgroup of b_{2} )

assume A37: H1 = fs . n ; :: thesis: ( H2 = fs . (n + 1) implies b_{3} is normal StableSubgroup of b_{2} )

assume A38: H2 = fs . (n + 1) ; :: thesis: b_{3} is normal StableSubgroup of b_{2}

reconsider i = i, n = n as Nat ;

end;b

assume that

A25: n in dom fs and

A26: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds

b

A27: n in Seg (len fs) by A25, FINSEQ_1:def 3;

then A28: n <= k by A6, A3, FINSEQ_1:1;

reconsider n1 = n + 1 as Nat ;

A29: n + 1 in Seg (len fs) by A26, FINSEQ_1:def 3;

then A30: n1 <= k by A6, A3, FINSEQ_1:1;

A31: 0 + (len fs) < 1 + (len fs) by XREAL_1:6;

then A32: Seg (len fs) c= Seg (len s1) by A6, A2, A3, FINSEQ_1:5;

then n in Seg (len s1) by A27;

then A33: n in dom s1 by FINSEQ_1:def 3;

n1 in Seg (len s1) by A29, A32;

then A34: n1 in dom s1 by FINSEQ_1:def 3;

n1 <= len fs by A29, FINSEQ_1:1;

then n1 < len s1 by A6, A2, A3, A31, XXREAL_0:2;

then n1 + 1 <= k + 1 by A2, NAT_1:13;

then Seg (n1 + 1) c= Seg (len s1) by A2, FINSEQ_1:5;

then A35: Seg (n1 + 1) c= dom s1 by FINSEQ_1:def 3;

A36: n1 + 1 in Seg (n1 + 1) by FINSEQ_1:4;

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies b

assume A37: H1 = fs . n ; :: thesis: ( H2 = fs . (n + 1) implies b

assume A38: H2 = fs . (n + 1) ; :: thesis: b

reconsider i = i, n = n as Nat ;

per cases
( n < i or n >= i )
;

end;

suppose A39:
n < i
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

then A40:
n1 <= i
by NAT_1:13;

reconsider n9 = n, i = i as Element of NAT by INT_1:3;

A41: (Del (s1,i)) . n9 = s1 . n9 by A39, FINSEQ_3:110;

end;reconsider n9 = n, i = i as Element of NAT by INT_1:3;

A41: (Del (s1,i)) . n9 = s1 . n9 by A39, FINSEQ_3:110;

per cases
( n1 < i or n1 = i )
by A40, XXREAL_0:1;

end;

suppose A44:
n >= i
; :: thesis: b_{3} is normal StableSubgroup of b_{2}

reconsider n9 = n, i = i as Element of NAT by INT_1:3;

A45: (Del (s1,i)) . n9 = s1 . (n9 + 1) by A1, A2, A28, A44, FINSEQ_3:111;

reconsider n19 = n1, i = i, k = k as Element of NAT by INT_1:3;

0 + n <= n + 1 by XREAL_1:6;

then A46: i <= n19 by A44, XXREAL_0:2;

n19 <= k by A6, A3, A29, FINSEQ_1:1;

then (Del (s1,i)) . n19 = s1 . (n19 + 1) by A1, A2, A46, FINSEQ_3:111;

hence H2 is normal StableSubgroup of H1 by A6, A37, A38, A34, A35, A36, A45, Def28; :: thesis: verum

end;A45: (Del (s1,i)) . n9 = s1 . (n9 + 1) by A1, A2, A28, A44, FINSEQ_3:111;

reconsider n19 = n1, i = i, k = k as Element of NAT by INT_1:3;

0 + n <= n + 1 by XREAL_1:6;

then A46: i <= n19 by A44, XXREAL_0:2;

n19 <= k by A6, A3, A29, FINSEQ_1:1;

then (Del (s1,i)) . n19 = s1 . (n19 + 1) by A1, A2, A46, FINSEQ_3:111;

hence H2 is normal StableSubgroup of H1 by A6, A37, A38, A34, A35, A36, A45, Def28; :: thesis: verum

then fs . (len fs) = s1 . (len s1) by A1, A6, A2, A3, FINSEQ_3:111;

then fs . (len fs) = (1). G by Def28;

hence fs is composition_series by A21, A24; :: thesis: verum