let O be set ; :: thesis: for G1, G2 being GroupWithOperators of O

for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let G1, G2 be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s1 be CompositionSeries of G1; :: thesis: for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s2 be CompositionSeries of G2; :: thesis: ( not s1 is empty & not s2 is empty implies ( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O ) )

assume that

A1: not s1 is empty and

A2: not s2 is empty ; :: thesis: ( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

set f2 = the_series_of_quotients_of s2;

set f1 = the_series_of_quotients_of s1;

A30: len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A29;

for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let G1, G2 be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s1 be CompositionSeries of G1; :: thesis: for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds

( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

let s2 be CompositionSeries of G2; :: thesis: ( not s1 is empty & not s2 is empty implies ( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O ) )

assume that

A1: not s1 is empty and

A2: not s2 is empty ; :: thesis: ( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

set f2 = the_series_of_quotients_of s2;

set f1 = the_series_of_quotients_of s1;

hereby :: thesis: ( ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O implies s1 is_equivalent_with s2 )

given p being Permutation of (dom (the_series_of_quotients_of s1)) such that A29:
the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O
; :: thesis: s1 is_equivalent_with s2assume A3:
s1 is_equivalent_with s2
; :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

then A4: len s1 = len s2 ;

end;then A4: len s1 = len s2 ;

per cases
( len s1 <= 1 or len s1 > 1 )
;

end;

suppose A5:
len s1 <= 1
; :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;

set p = the Permutation of (dom (the_series_of_quotients_of s1));

reconsider pf = the Permutation of (dom (the_series_of_quotients_of s1)) as Permutation of (dom fs1) ;

fs1 = {} by A5, Def33;

then A6: for H1, H2 being GroupWithOperators of O

for i, j being Nat st i in dom fs1 & j = (pf ") . i & H1 = fs1 . i & H2 = fs2 . j holds

H1,H2 are_isomorphic ;

take p = the Permutation of (dom (the_series_of_quotients_of s1)); :: thesis: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

fs2 = {} by A4, A5, Def33;

then len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A5, Def33;

hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6; :: thesis: verum

end;set p = the Permutation of (dom (the_series_of_quotients_of s1));

reconsider pf = the Permutation of (dom (the_series_of_quotients_of s1)) as Permutation of (dom fs1) ;

fs1 = {} by A5, Def33;

then A6: for H1, H2 being GroupWithOperators of O

for i, j being Nat st i in dom fs1 & j = (pf ") . i & H1 = fs1 . i & H2 = fs2 . j holds

H1,H2 are_isomorphic ;

take p = the Permutation of (dom (the_series_of_quotients_of s1)); :: thesis: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

fs2 = {} by A4, A5, Def33;

then len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A5, Def33;

hence the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6; :: thesis: verum

suppose A7:
len s1 > 1
; :: thesis: ex p9 being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O

set n = (len s1) - 1;

(len s1) - 1 > 1 - 1 by A7, XREAL_1:9;

then (len s1) - 1 in NAT by INT_1:3;

then reconsider n = (len s1) - 1 as Nat ;

n + 1 = len s1 ;

then consider p being Permutation of (Seg n) such that

A8: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic by A3;

A9: len s1 = (len (the_series_of_quotients_of s1)) + 1 by A7, Def33;

then dom (the_series_of_quotients_of s1) = Seg n by FINSEQ_1:def 3;

then reconsider p9 = p " as Permutation of (dom (the_series_of_quotients_of s1)) ;

reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;

A10: len s2 = (len (the_series_of_quotients_of s2)) + 1 by A4, A7, Def33;

reconsider pf = p9 as Permutation of (dom fs1) ;

take p9 = p9; :: thesis: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O

A11: pf " = p by FUNCT_1:43;

end;(len s1) - 1 > 1 - 1 by A7, XREAL_1:9;

then (len s1) - 1 in NAT by INT_1:3;

then reconsider n = (len s1) - 1 as Nat ;

n + 1 = len s1 ;

then consider p being Permutation of (Seg n) such that

A8: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic by A3;

A9: len s1 = (len (the_series_of_quotients_of s1)) + 1 by A7, Def33;

then dom (the_series_of_quotients_of s1) = Seg n by FINSEQ_1:def 3;

then reconsider p9 = p " as Permutation of (dom (the_series_of_quotients_of s1)) ;

reconsider fs1 = the_series_of_quotients_of s1, fs2 = the_series_of_quotients_of s2 as FinSequence ;

A10: len s2 = (len (the_series_of_quotients_of s2)) + 1 by A4, A7, Def33;

reconsider pf = p9 as Permutation of (dom fs1) ;

take p9 = p9; :: thesis: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O

A11: pf " = p by FUNCT_1:43;

now :: thesis: for H19, H29 being GroupWithOperators of O

for i, j being Nat st i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j holds

H19,H29 are_isomorphic

hence
the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,O
by A4, A9, A10; :: thesis: verumfor i, j being Nat st i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j holds

H19,H29 are_isomorphic

let H19, H29 be GroupWithOperators of O; :: thesis: for i, j being Nat st i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j holds

H19,H29 are_isomorphic

let i, j be Nat; :: thesis: ( i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

set H1 = s1 . i;

set H2 = s2 . j;

set N1 = s1 . (i + 1);

set N2 = s2 . (j + 1);

assume A12: i in dom fs1 ; :: thesis: ( j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

then A13: i in Seg (len fs1) by FINSEQ_1:def 3;

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

A15: i <= len fs1 by A13, FINSEQ_1:1;

then A16: i + 1 <= (len fs1) + 1 by XREAL_1:6;

0 + i < 1 + i by XREAL_1:6;

then 1 <= i + 1 by A14, XXREAL_0:2;

then i + 1 in Seg (len s1) by A9, A16;

then A17: i + 1 in dom s1 by FINSEQ_1:def 3;

assume A18: j = (pf ") . i ; :: thesis: ( H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

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

then i <= len s1 by A9, A15, XXREAL_0:2;

then i in Seg (len s1) by A14;

then A19: i in dom s1 by FINSEQ_1:def 3;

then reconsider H1 = s1 . i, N1 = s1 . (i + 1) as Element of the_stable_subgroups_of G1 by A17, FINSEQ_2:11;

reconsider H1 = H1, N1 = N1 as StableSubgroup of G1 by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A19, A17, Def28;

assume that

A20: H19 = fs1 . i and

A21: H29 = fs2 . j ; :: thesis: H19,H29 are_isomorphic

i in dom p by A9, A13, FUNCT_2:def 1;

then A22: j in rng p by A11, A18, FUNCT_1:3;

then A23: 1 <= j by FINSEQ_1:1;

A24: j <= len fs2 by A4, A10, A22, FINSEQ_1:1;

then A25: j + 1 <= (len fs2) + 1 by XREAL_1:6;

0 + j < 1 + j by XREAL_1:6;

then 1 <= j + 1 by A23, XXREAL_0:2;

then j + 1 in Seg (len s2) by A10, A25;

then A26: j + 1 in dom s2 by FINSEQ_1:def 3;

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

then j <= len s2 by A10, A24, XXREAL_0:2;

then j in Seg (len s2) by A23;

then A27: j in dom s2 by FINSEQ_1:def 3;

then reconsider H2 = s2 . j, N2 = s2 . (j + 1) as Element of the_stable_subgroups_of G2 by A26, FINSEQ_2:11;

reconsider H2 = H2, N2 = N2 as StableSubgroup of G2 by Def11;

reconsider N2 = N2 as normal StableSubgroup of H2 by A27, A26, Def28;

dom fs1 = Seg n by A9, FINSEQ_1:def 3;

then ( 1 <= i & i <= n ) by A12, FINSEQ_1:1;

then A28: H1 ./. N1,H2 ./. N2 are_isomorphic by A8, A11, A18;

j in Seg (len (the_series_of_quotients_of s2)) by A4, A10, A22;

then j in dom fs2 by FINSEQ_1:def 3;

then H2 ./. N2 = H29 by A4, A7, A21, Def33;

hence H19,H29 are_isomorphic by A7, A12, A20, A28, Def33; :: thesis: verum

end;H19,H29 are_isomorphic

let i, j be Nat; :: thesis: ( i in dom fs1 & j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

set H1 = s1 . i;

set H2 = s2 . j;

set N1 = s1 . (i + 1);

set N2 = s2 . (j + 1);

assume A12: i in dom fs1 ; :: thesis: ( j = (pf ") . i & H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

then A13: i in Seg (len fs1) by FINSEQ_1:def 3;

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

A15: i <= len fs1 by A13, FINSEQ_1:1;

then A16: i + 1 <= (len fs1) + 1 by XREAL_1:6;

0 + i < 1 + i by XREAL_1:6;

then 1 <= i + 1 by A14, XXREAL_0:2;

then i + 1 in Seg (len s1) by A9, A16;

then A17: i + 1 in dom s1 by FINSEQ_1:def 3;

assume A18: j = (pf ") . i ; :: thesis: ( H19 = fs1 . i & H29 = fs2 . j implies H19,H29 are_isomorphic )

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

then i <= len s1 by A9, A15, XXREAL_0:2;

then i in Seg (len s1) by A14;

then A19: i in dom s1 by FINSEQ_1:def 3;

then reconsider H1 = s1 . i, N1 = s1 . (i + 1) as Element of the_stable_subgroups_of G1 by A17, FINSEQ_2:11;

reconsider H1 = H1, N1 = N1 as StableSubgroup of G1 by Def11;

reconsider N1 = N1 as normal StableSubgroup of H1 by A19, A17, Def28;

assume that

A20: H19 = fs1 . i and

A21: H29 = fs2 . j ; :: thesis: H19,H29 are_isomorphic

i in dom p by A9, A13, FUNCT_2:def 1;

then A22: j in rng p by A11, A18, FUNCT_1:3;

then A23: 1 <= j by FINSEQ_1:1;

A24: j <= len fs2 by A4, A10, A22, FINSEQ_1:1;

then A25: j + 1 <= (len fs2) + 1 by XREAL_1:6;

0 + j < 1 + j by XREAL_1:6;

then 1 <= j + 1 by A23, XXREAL_0:2;

then j + 1 in Seg (len s2) by A10, A25;

then A26: j + 1 in dom s2 by FINSEQ_1:def 3;

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

then j <= len s2 by A10, A24, XXREAL_0:2;

then j in Seg (len s2) by A23;

then A27: j in dom s2 by FINSEQ_1:def 3;

then reconsider H2 = s2 . j, N2 = s2 . (j + 1) as Element of the_stable_subgroups_of G2 by A26, FINSEQ_2:11;

reconsider H2 = H2, N2 = N2 as StableSubgroup of G2 by Def11;

reconsider N2 = N2 as normal StableSubgroup of H2 by A27, A26, Def28;

dom fs1 = Seg n by A9, FINSEQ_1:def 3;

then ( 1 <= i & i <= n ) by A12, FINSEQ_1:1;

then A28: H1 ./. N1,H2 ./. N2 are_isomorphic by A8, A11, A18;

j in Seg (len (the_series_of_quotients_of s2)) by A4, A10, A22;

then j in dom fs2 by FINSEQ_1:def 3;

then H2 ./. N2 = H29 by A4, A7, A21, Def33;

hence H19,H29 are_isomorphic by A7, A12, A20, A28, Def33; :: thesis: verum

A30: len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) by A29;

per cases
( len s1 <= 1 or len s1 > 1 )
;

end;

suppose A31:
len s1 <= 1
; :: thesis: s1 is_equivalent_with s2

A32:
len s1 >= 0 + 1
by A1, NAT_1:13;

hence s1 is_equivalent_with s2 by A33; :: thesis: verum

end;A33: now :: thesis: for n being Nat st n + 1 = len s1 holds

ex p being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

A36:
the_series_of_quotients_of s1 = {}
by A31, Def33;ex p being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let n be Nat; :: thesis: ( n + 1 = len s1 implies ex p being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic )

set p = the Permutation of (Seg n);

assume n + 1 = len s1 ; :: thesis: ex p being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

then n + 1 = 1 by A31, A32, XXREAL_0:1;

then A34: n = 0 ;

take p = the Permutation of (Seg n); :: thesis: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H1 be StableSubgroup of G1; :: thesis: for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H2 be StableSubgroup of G2; :: thesis: for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N1 be normal StableSubgroup of H1; :: thesis: for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N2 be normal StableSubgroup of H2; :: thesis: for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A35: ( 1 <= i & i <= n ) and

j = p . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

H1 = s1 . i and

H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

N1 = s1 . (i + 1) and

N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic

thus H1 ./. N1,H2 ./. N2 are_isomorphic by A34, A35; :: thesis: verum

end;for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic )

set p = the Permutation of (Seg n);

assume n + 1 = len s1 ; :: thesis: ex p being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

then n + 1 = 1 by A31, A32, XXREAL_0:1;

then A34: n = 0 ;

take p = the Permutation of (Seg n); :: thesis: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H1 be StableSubgroup of G1; :: thesis: for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H2 be StableSubgroup of G2; :: thesis: for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N1 be normal StableSubgroup of H1; :: thesis: for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N2 be normal StableSubgroup of H2; :: thesis: for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A35: ( 1 <= i & i <= n ) and

j = p . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

H1 = s1 . i and

H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

N1 = s1 . (i + 1) and

N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic

thus H1 ./. N1,H2 ./. N2 are_isomorphic by A34, A35; :: thesis: verum

now :: thesis: not len s2 <> 1

then
len s1 = len s2
by A31, A32, XXREAL_0:1;assume A37:
len s2 <> 1
; :: thesis: contradiction

len s2 >= 0 + 1 by A2, NAT_1:13;

then len s2 > 1 by A37, XXREAL_0:1;

then (len (the_series_of_quotients_of s2)) + 1 > 0 + 1 by Def33;

hence contradiction by A30, A36; :: thesis: verum

end;len s2 >= 0 + 1 by A2, NAT_1:13;

then len s2 > 1 by A37, XXREAL_0:1;

then (len (the_series_of_quotients_of s2)) + 1 > 0 + 1 by Def33;

hence contradiction by A30, A36; :: thesis: verum

hence s1 is_equivalent_with s2 by A33; :: thesis: verum

suppose A38:
len s1 > 1
; :: thesis: s1 is_equivalent_with s2

then A39:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by Def33;

hence s1 is_equivalent_with s2 by A41; :: thesis: verum

end;A40: now :: thesis: not len s2 <= 1

assume
len s2 <= 1
; :: thesis: contradiction

then the_series_of_quotients_of s2 = {} by Def33;

then len (the_series_of_quotients_of s2) = 0 ;

hence contradiction by A30, A38, A39; :: thesis: verum

end;then the_series_of_quotients_of s2 = {} by Def33;

then len (the_series_of_quotients_of s2) = 0 ;

hence contradiction by A30, A38, A39; :: thesis: verum

A41: now :: thesis: for n being Nat st n + 1 = len s1 holds

ex p9 being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

len s1 = len s2
by A30, A39, A40, Def33;ex p9 being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let n be Nat; :: thesis: ( n + 1 = len s1 implies ex p9 being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic )

assume A42: n + 1 = len s1 ; :: thesis: ex p9 being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

then A43: dom (the_series_of_quotients_of s1) = Seg n by A39, FINSEQ_1:def 3;

then reconsider p9 = p " as Permutation of (Seg n) ;

take p9 = p9; :: thesis: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H1 be StableSubgroup of G1; :: thesis: for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H2 be StableSubgroup of G2; :: thesis: for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N1 be normal StableSubgroup of H1; :: thesis: for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N2 be normal StableSubgroup of H2; :: thesis: for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume ( 1 <= i & i <= n ) ; :: thesis: ( j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

then A44: i in dom (the_series_of_quotients_of s1) by A43;

assume A45: j = p9 . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A46: H1 = s1 . i and

A47: H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A48: N1 = s1 . (i + 1) and

A49: N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic

i in dom p9 by A44, FUNCT_2:def 1;

then j in rng p9 by A45, FUNCT_1:3;

then j in Seg n ;

then j in dom (the_series_of_quotients_of s2) by A30, A39, A42, FINSEQ_1:def 3;

then A50: (the_series_of_quotients_of s2) . j = H2 ./. N2 by A40, A47, A49, Def33;

(the_series_of_quotients_of s1) . i = H1 ./. N1 by A38, A44, A46, A48, Def33;

hence H1 ./. N1,H2 ./. N2 are_isomorphic by A29, A44, A45, A50; :: thesis: verum

end;for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic )

assume A42: n + 1 = len s1 ; :: thesis: ex p9 being Permutation of (Seg n) st

for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

then A43: dom (the_series_of_quotients_of s1) = Seg n by A39, FINSEQ_1:def 3;

then reconsider p9 = p " as Permutation of (Seg n) ;

take p9 = p9; :: thesis: for H1 being StableSubgroup of G1

for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H1 be StableSubgroup of G1; :: thesis: for H2 being StableSubgroup of G2

for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let H2 be StableSubgroup of G2; :: thesis: for N1 being normal StableSubgroup of H1

for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N1 be normal StableSubgroup of H1; :: thesis: for N2 being normal StableSubgroup of H2

for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let N2 be normal StableSubgroup of H2; :: thesis: for i, j being Nat st 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds

H1 ./. N1,H2 ./. N2 are_isomorphic

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume ( 1 <= i & i <= n ) ; :: thesis: ( j = p9 . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

then A44: i in dom (the_series_of_quotients_of s1) by A43;

assume A45: j = p9 . i ; :: thesis: ( H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A46: H1 = s1 . i and

A47: H2 = s2 . j ; :: thesis: ( N1 = s1 . (i + 1) & N2 = s2 . (j + 1) implies H1 ./. N1,H2 ./. N2 are_isomorphic )

assume that

A48: N1 = s1 . (i + 1) and

A49: N2 = s2 . (j + 1) ; :: thesis: H1 ./. N1,H2 ./. N2 are_isomorphic

i in dom p9 by A44, FUNCT_2:def 1;

then j in rng p9 by A45, FUNCT_1:3;

then j in Seg n ;

then j in dom (the_series_of_quotients_of s2) by A30, A39, A42, FINSEQ_1:def 3;

then A50: (the_series_of_quotients_of s2) . j = H2 ./. N2 by A40, A47, A49, Def33;

(the_series_of_quotients_of s1) . i = H1 ./. N1 by A38, A44, A46, A48, Def33;

hence H1 ./. N1,H2 ./. N2 are_isomorphic by A29, A44, A45, A50; :: thesis: verum

hence s1 is_equivalent_with s2 by A41; :: thesis: verum