let O be set ; for G being GroupWithOperators of O
for s1 being CompositionSeries of G holds s1 is_equivalent_with s1
let G be GroupWithOperators of O; for s1 being CompositionSeries of G holds s1 is_equivalent_with s1
let s1 be CompositionSeries of G; s1 is_equivalent_with s1
per cases
( s1 is empty or not s1 is empty )
;
suppose A1:
not
s1 is
empty
;
s1 is_equivalent_with s1set f1 =
the_series_of_quotients_of s1;
now ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,Oset p =
id (dom (the_series_of_quotients_of s1));
reconsider p =
id (dom (the_series_of_quotients_of s1)) as
Function of
(dom (the_series_of_quotients_of s1)),
(dom (the_series_of_quotients_of s1)) ;
p is
onto
;
then reconsider p =
p as
Permutation of
(dom (the_series_of_quotients_of s1)) ;
take p =
p;
the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,OA2:
now for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom (the_series_of_quotients_of s1) & j = (p ") . i & H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s1) . j holds
H1,H2 are_isomorphic let H1,
H2 be
GroupWithOperators of
O;
for i, j being Nat st i in dom (the_series_of_quotients_of s1) & j = (p ") . i & H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s1) . j holds
H1,H2 are_isomorphic let i,
j be
Nat;
( i in dom (the_series_of_quotients_of s1) & j = (p ") . i & H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s1) . j implies H1,H2 are_isomorphic )assume A3:
(
i in dom (the_series_of_quotients_of s1) &
j = (p ") . i )
;
( H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s1) . j implies H1,H2 are_isomorphic )A4:
p " = p
by FUNCT_1:45;
assume
(
H1 = (the_series_of_quotients_of s1) . i &
H2 = (the_series_of_quotients_of s1) . j )
;
H1,H2 are_isomorphic hence
H1,
H2 are_isomorphic
by A3, A4, FUNCT_1:18;
verum end; thus
the_series_of_quotients_of s1,
the_series_of_quotients_of s1 are_equivalent_under p,
O
by A2;
verum end; hence
s1 is_equivalent_with s1
by A1, Th108;
verum end; end;