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

per cases ( s1 is empty or not s1 is empty ) ;

suppose s1 is empty ; :: thesis: s1 is_equivalent_with s1

hence s1 is_equivalent_with s1 by Th107; :: thesis: verum

end;

suppose A1: not s1 is empty ; :: thesis: s1 is_equivalent_with s1

set f1 = the_series_of_quotients_of s1;

now

set 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)) ;
rng p = dom (the_series_of_quotients_of s1) by RELAT_1:45;
then p is onto by FUNCT_2:def 3;
then reconsider p = p as Permutation of (dom (the_series_of_quotients_of s1)) ;
take p = p; :: thesis: the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,O

A2: now

let H1, H2 be GroupWithOperators of O; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: H1,H2 are_isomorphic
hence H1,H2 are_isomorphic by A3, A4, FUNCT_1:18; :: thesis: verum

end;

len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s1) ;
hence the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,O by A2, Def37; :: thesis: verum

end;

hence s1 is_equivalent_with s1 by A1, Th108; :: thesis: verum

end;

end;