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:
per cases ( s1 is empty or not s1 is empty ) ;
suppose s1 is empty ; :: thesis:
end;
suppose A1: not s1 is empty ; :: thesis:
set f1 = the_series_of_quotients_of s1;
now :: thesis: ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,O
set p = id ();
reconsider p = id () as Function of (),() ;
p is onto ;
then reconsider p = p as Permutation of () ;
take p = p; :: thesis:
A2: now :: thesis: for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom & j = (p ") . i & H1 = . i & H2 = . j holds
H1,H2 are_isomorphic
let H1, H2 be GroupWithOperators of O; :: thesis: for i, j being Nat st i in dom & j = (p ") . i & H1 = . i & H2 = . j holds
H1,H2 are_isomorphic

let i, j be Nat; :: thesis: ( i in dom & j = (p ") . i & H1 = . i & H2 = . j implies H1,H2 are_isomorphic )
assume A3: ( i in dom & j = (p ") . i ) ; :: thesis: ( H1 = . i & H2 = . j implies H1,H2 are_isomorphic )
A4: p " = p by FUNCT_1:45;
assume ( H1 = . i & H2 = . j ) ; :: thesis: H1,H2 are_isomorphic
hence H1,H2 are_isomorphic by ; :: 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 ; :: thesis: verum
end;
end;