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 ;
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 ;
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 ;
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 ;
then j2 = j1 mod l99 by ;
hence contradiction by A8, A12, NAT_D:25; :: thesis: verum
end;
suppose j1 <> l99 ; :: thesis: j1 = j2
then j1 < l99 by ;
then A13: j1 = j2 mod l99 by ;
per cases ( j2 = l99 or j2 <> l99 ) ;
suppose j2 = l99 ; :: thesis: j1 = j2
hence j1 = j2 by ; :: thesis: verum
end;
suppose j2 <> l99 ; :: thesis: j1 = j2
then j2 < l99 by ;
hence j1 = j2 by ; :: thesis: verum
end;
end;
end;
end;
end;
hence j1 = j2 ; :: thesis: i1 = i2
i19 * (l99 / l99) = (i29 * l99) / l99 by ;
then i19 * 1 = i29 * 1 by ;
hence i1 = i2 ; :: thesis: verum