let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G
for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
let s1, s2 be CompositionSeries of G; :: thesis: for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
let k, l be Nat; :: thesis: ( k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) )
assume A1: k in Seg l ; :: thesis: ( not len s1 > 1 or not len s2 > 1 or not l = (((len s1) - 1) * ((len s2) - 1)) + 1 or k = (((len s1) - 1) * ((len s2) - 1)) + 1 or ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) )
then A2: ( 1 <= k & k <= l ) by FINSEQ_1:3;
assume A3: ( len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ; :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 or ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) )
assume not k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
then A4: k < l by A2, A3, XXREAL_0:1;
set l' = (len s1) - 1;
(len s1) - 1 > 1 - 1 by A3, XREAL_1:11;
then reconsider l' = (len s1) - 1 as Element of NAT by INT_1:16;
set l'' = (len s2) - 1;
A5: (len s2) - 1 > 1 - 1 by A3, XREAL_1:11;
then reconsider l'' = (len s2) - 1 as Element of NAT by INT_1:16;
( (len s1) + 1 > 1 + 1 & (len s2) + 1 > 1 + 1 ) by A3, XREAL_1:8;
then ( len s1 >= 2 & len s2 >= 2 ) by NAT_1:13;
then A6: ( (len s1) - 1 >= 2 - 1 & (len s2) - 1 >= 2 - 1 ) by XREAL_1:11;
A7: k = ((k div l'') * l'') + (k mod l'') by A5, NAT_D:2;

per cases ( k mod l'' = 0 or k mod l'' <> 0 ) ;

suppose A8: k mod l'' = 0 ; :: thesis: ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )

set j = l'';
set i = k div l'';
take k div l'' ; :: thesis: ex j being Nat st
( k = (((k div l'') - 1) * ((len s2) - 1)) + j & 1 <= k div l'' & k div l'' <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
take l'' ; :: thesis: ( k = (((k div l'') - 1) * ((len s2) - 1)) + l'' & 1 <= k div l'' & k div l'' <= (len s1) - 1 & 1 <= l'' & l'' <= (len s2) - 1 )
thus k = (((k div l'') - 1) * ((len s2) - 1)) + l'' by A7, A8; :: thesis: ( 1 <= k div l'' & k div l'' <= (len s1) - 1 & 1 <= l'' & l'' <= (len s2) - 1 )
k div l'' <> 0 by A1, A7, A8, FINSEQ_1:3;
then k div l'' > 0 ;
then (k div l'') + 1 > 0 + 1 by XREAL_1:8;
hence 1 <= k div l'' by NAT_1:13; :: thesis: ( k div l'' <= (len s1) - 1 & 1 <= l'' & l'' <= (len s2) - 1 )
(k div l'') * l'' <= ((len s1) - 1) * l'' by A3, A4, A7, A8, INT_1:20;
then ((k div l'') * l'') / l'' <= (((len s1) - 1) * l'') / l'' by XREAL_1:74;
then k div l'' <= (((len s1) - 1) * l'') / l'' by A5, XCMPLX_1:90;
hence k div l'' <= (len s1) - 1 by A5, XCMPLX_1:90; :: thesis: ( 1 <= l'' & l'' <= (len s2) - 1 )
thus ( 1 <= l'' & l'' <= (len s2) - 1 ) by A6; :: thesis: verum

end;

suppose A9: k mod l'' <> 0 ; :: thesis: ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )

set j = k mod l'';
set i = (k div l'') + 1;
take (k div l'') + 1 ; :: thesis: ex j being Nat st
( k = ((((k div l'') + 1) - 1) * ((len s2) - 1)) + j & 1 <= (k div l'') + 1 & (k div l'') + 1 <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
take k mod l'' ; :: thesis: ( k = ((((k div l'') + 1) - 1) * ((len s2) - 1)) + (k mod l'') & 1 <= (k div l'') + 1 & (k div l'') + 1 <= (len s1) - 1 & 1 <= k mod l'' & k mod l'' <= (len s2) - 1 )
thus k = ((((k div l'') + 1) - 1) * ((len s2) - 1)) + (k mod l'') by A5, NAT_D:2; :: thesis: ( 1 <= (k div l'') + 1 & (k div l'') + 1 <= (len s1) - 1 & 1 <= k mod l'' & k mod l'' <= (len s2) - 1 )
0 + 1 <= (k div l'') + 1 by XREAL_1:8;
hence 1 <= (k div l'') + 1 ; :: thesis: ( (k div l'') + 1 <= (len s1) - 1 & 1 <= k mod l'' & k mod l'' <= (len s2) - 1 )
A10: k <> l' * l'' by A9, NAT_D:13;
k + 1 <= l by A4, INT_1:20;
then (k + 1) - 1 <= l - 1 by XREAL_1:11;
then A11: k < ((len s1) - 1) * l'' by A3, A10, XXREAL_0:1;
(k mod l'') + (l'' * (k div l'')) >= 0 + (l'' * (k div l'')) by XREAL_1:8;
then (k div l'') * l'' <= k by A5, NAT_D:2;
then (k div l'') * l'' < ((len s1) - 1) * l'' by A11, XXREAL_0:2;
then ((k div l'') * l'') / l'' < (((len s1) - 1) * l'') / l'' by A5, XREAL_1:76;
then k div l'' < (((len s1) - 1) * l'') / l'' by A5, XCMPLX_1:90;
then k div l'' < (len s1) - 1 by A5, XCMPLX_1:90;
hence (k div l'') + 1 <= (len s1) - 1 by INT_1:20; :: thesis: ( 1 <= k mod l'' & k mod l'' <= (len s2) - 1 )
k mod l'' > 0 by A9;
then (k mod l'') + 1 > 0 + 1 by XREAL_1:8;
hence 1 <= k mod l'' by NAT_1:13; :: thesis: k mod l'' <= (len s2) - 1
thus k mod l'' <= (len s2) - 1 by A5, NAT_D:1; :: thesis: verum

end;

end;