let O be set ; :: thesis: for G being GroupWithOperators of O
for i1, j1, i2, j2 being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )
let G be GroupWithOperators of O; :: thesis: for i1, j1, i2, j2 being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )
let i1, j1, i2, j2 be Nat; :: thesis: for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )
let s1, s2 be CompositionSeries of G; :: thesis: ( len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 implies ( j1 = j2 & i1 = i2 ) )
set l99 = (len s2) - 1;
set i19 = i1 - 1;
set i29 = i2 - 1;
assume len s2 > 1 ; :: thesis: ( not ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 or not 1 <= i1 or not 1 <= j1 or not j1 <= (len s2) - 1 or not 1 <= i2 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
then A1: (len s2) - 1 > 1 - 1 by XREAL_1:9;
then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;
A2: l99 / l99 = 1 by A1, XCMPLX_1:60;
assume A3: ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 ; :: thesis: ( not 1 <= i1 or not 1 <= j1 or not j1 <= (len s2) - 1 or not 1 <= i2 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
assume that
A4: 1 <= i1 and
A5: 1 <= j1 and
A6: j1 <= (len s2) - 1 ; :: thesis: ( not 1 <= i2 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
i1 - 1 >= 1 - 1 by A4, XREAL_1:9;
then reconsider i19 = i1 - 1 as Element of NAT by INT_1:3;
assume that
A7: 1 <= i2 and
A8: 1 <= j2 and
A9: j2 <= (len s2) - 1 ; :: thesis: ( j1 = j2 & i1 = i2 )
i2 - 1 >= 1 - 1 by A7, XREAL_1:9;
then reconsider i29 = i2 - 1 as Element of NAT by INT_1:3;
A10: j1 mod l99 = ((i19 * l99) + j1) mod l99 by NAT_D:21
.= ((i29 * l99) + j2) mod l99 by A3
.= j2 mod l99 by NAT_D:21 ;
A11: j1 = j2

proof

per cases ( j1 = l99 or j1 <> l99 ) ;

suppose A12: j1 = l99 ; :: thesis: j1 = j2

assume j2 <> j1 ; :: thesis: contradiction
then j2 < l99 by A9, A12, XXREAL_0:1;
then j2 = j1 mod l99 by A10, NAT_D:24;
hence contradiction by A8, A12, NAT_D:25; :: thesis: verum

end;

suppose j1 <> l99 ; :: thesis: j1 = j2

then j1 < l99 by A6, XXREAL_0:1;
then A13: j1 = j2 mod l99 by A10, NAT_D:24;

per cases ( j2 = l99 or j2 <> l99 ) ;

suppose j2 = l99 ; :: thesis: j1 = j2

hence j1 = j2 by A5, A13, NAT_D:25; :: thesis: verum

end;

suppose j2 <> l99 ; :: thesis: j1 = j2

then j2 < l99 by A9, XXREAL_0:1;
hence j1 = j2 by A13, NAT_D:24; :: thesis: verum

end;

end;

end;

end;

end;

hence j1 = j2 ; :: thesis: i1 = i2
i19 * (l99 / l99) = (i29 * l99) / l99 by A3, A11, XCMPLX_1:74;
then i19 * 1 = i29 * 1 by A2, XCMPLX_1:74;
hence i1 = i2 ; :: thesis: verum