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

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

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

hence
j1 = j2
; :: thesis: i1 = i2per cases
( j1 = l99 or j1 <> l99 )
;

end;

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

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

end;

end;

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