let O be set ; 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; 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; 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; ( 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
; ( 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 ( 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 )
assume A3:
s1 is_equivalent_with s2
;
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,Othen A4:
len s1 = len s2
;
per cases
( len s1 <= 1 or len s1 > 1 )
;
suppose A5:
len s1 <= 1
;
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,Oreconsider 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));
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;
verum end; suppose A7:
len s1 > 1
;
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,Oset 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;
the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p9,OA11:
pf " = p
by FUNCT_1:43;
now 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 let H19,
H29 be
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 let i,
j be
Nat;
( 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
;
( 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
;
( 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
;
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;
verum end; hence
the_series_of_quotients_of s1,
the_series_of_quotients_of s2 are_equivalent_under p9,
O
by A4, A9, A10;
verum end; end;
end;
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
; s1 is_equivalent_with s2
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 )
;
suppose A31:
len s1 <= 1
;
s1 is_equivalent_with s2A32:
len s1 >= 0 + 1
by A1, NAT_1:13;
A33:
now 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 let n be
Nat;
( 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
;
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);
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;
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;
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;
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;
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;
( 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
;
( 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
;
( 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)
;
H1 ./. N1,H2 ./. N2 are_isomorphic thus
H1 ./. N1,
H2 ./. N2 are_isomorphic
by A34, A35;
verum end; A36:
the_series_of_quotients_of s1 = {}
by A31, Def33;
then
len s1 = len s2
by A31, A32, XXREAL_0:1;
hence
s1 is_equivalent_with s2
by A33;
verum end; suppose A38:
len s1 > 1
;
s1 is_equivalent_with s2then A39:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by Def33;
A41:
now 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 let n be
Nat;
( 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
;
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;
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;
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;
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;
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;
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;
( 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 )
;
( 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
;
( 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
;
( 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)
;
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;
verum end;
len s1 = len s2
by A30, A39, A40, Def33;
hence
s1 is_equivalent_with s2
by A41;
verum end; end;