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