for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2 ;