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 ; :: thesis: verum

end;

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

set f1 = the_series_of_quotients_of s1;

now :: 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 s1 are_equivalent_under p,O

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)) ;
p is onto ;
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 :: thesis: 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; :: 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;

thus the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,O by A2; :: thesis: verum

end;

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

end;

end;