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 s1 > 1 & len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & i2 <= (len s1) - 1 & 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 s1 > 1 & len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & i2 <= (len s1) - 1 & 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 s1 > 1 & len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & i2 <= (len s1) - 1 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )
let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & i2 <= (len s1) - 1 & 1 <= j2 & j2 <= (len s2) - 1 implies ( j1 = j2 & i1 = i2 ) )
assume A1: ( len s1 > 1 & len s2 > 1 ) ; :: thesis: ( not ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 or not 1 <= i1 or not i1 <= (len s1) - 1 or not 1 <= j1 or not j1 <= (len s2) - 1 or not 1 <= i2 or not i2 <= (len s1) - 1 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
assume A2: ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 ; :: thesis: ( not 1 <= i1 or not i1 <= (len s1) - 1 or not 1 <= j1 or not j1 <= (len s2) - 1 or not 1 <= i2 or not i2 <= (len s1) - 1 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
assume A3: ( 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 ) ; :: thesis: ( not 1 <= i2 or not i2 <= (len s1) - 1 or not 1 <= j2 or not j2 <= (len s2) - 1 or ( j1 = j2 & i1 = i2 ) )
assume A4: ( 1 <= i2 & i2 <= (len s1) - 1 & 1 <= j2 & j2 <= (len s2) - 1 ) ; :: thesis: ( j1 = j2 & i1 = i2 )
set l'' = (len s2) - 1;
A5: (len s2) - 1 > 1 - 1 by A1, XREAL_1:11;
then reconsider l'' = (len s2) - 1 as Element of NAT by INT_1:16;
set i1' = i1 - 1;
i1 - 1 >= 1 - 1 by A3, XREAL_1:11;
then reconsider i1' = i1 - 1 as Element of NAT by INT_1:16;
set i2' = i2 - 1;
i2 - 1 >= 1 - 1 by A4, XREAL_1:11;
then reconsider i2' = i2 - 1 as Element of NAT by INT_1:16;
A6: j1 mod l'' = ((i1' * l'') + j1) mod l'' by NAT_D:21
.= ((i2' * l'') + j2) mod l'' by A2
.= j2 mod l'' by NAT_D:21 ;
A7: j1 = j2

proof

per cases ( j1 = l'' or j1 <> l'' ) ;

suppose A8: j1 = l'' ; :: thesis: j1 = j2

assume j2 <> j1 ; :: thesis: contradiction
then j2 < l'' by A4, A8, XXREAL_0:1;
then j2 = j1 mod l'' by A6, NAT_D:24;
hence contradiction by A4, A8, NAT_D:25; :: thesis: verum

end;

suppose j1 <> l'' ; :: thesis: j1 = j2

then j1 < l'' by A3, XXREAL_0:1;
then A9: j1 = j2 mod l'' by A6, NAT_D:24;

per cases ( j2 = l'' or j2 <> l'' ) ;

suppose j2 = l'' ; :: thesis: j1 = j2

hence j1 = j2 by A3, A9, NAT_D:25; :: thesis: verum

end;

suppose j2 <> l'' ; :: thesis: j1 = j2

then j2 < l'' by A4, XXREAL_0:1;
hence j1 = j2 by A9, NAT_D:24; :: thesis: verum

end;

end;

end;

end;

end;

hence j1 = j2 ; :: thesis: i1 = i2
A10: l'' / l'' = 1 by A5, XCMPLX_1:60;
i1' * (l'' / l'') = (i2' * l'') / l'' by A2, A7, XCMPLX_1:75;
then i1' * 1 = i2' * 1 by A10, XCMPLX_1:75;
hence i1 = i2 ; :: thesis: verum