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

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 )
;

end;

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

set f1 = the_series_of_quotients_of s1;

end;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

hence
s1 is_equivalent_with s1
by A1, Th108; :: thesis: verumset 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

end;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

thus
the_series_of_quotients_of s1, the_series_of_quotients_of s1 are_equivalent_under p,O
by A2; :: thesis: verumfor 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;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