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 ) )
set l9 = (len s1) - 1;
set l99 = (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: k <= l by FINSEQ_1:1;
assume that
A3: len s1 > 1 and
A4: len s2 > 1 and
A5: 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 A6: k < l by A2, A5, XXREAL_0:1;
(len s2) + 1 > 1 + 1 by A4, XREAL_1:6;
then len s2 >= 2 by NAT_1:13;
then A7: (len s2) - 1 >= 2 - 1 by XREAL_1:9;
(len s1) - 1 > 1 - 1 by A3, XREAL_1:9;
then reconsider l9 = (len s1) - 1 as Element of NAT by INT_1:3;
A8: (len s2) - 1 > 1 - 1 by A4, XREAL_1:9;
then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;
A9: k = ((k div l99) * l99) + (k mod l99) by A8, NAT_D:2;
per cases ( k mod l99 = 0 or k mod l99 <> 0 ) ;
suppose A10: k mod l99 = 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 i = k div l99;
set j = l99;
take k div l99 ; :: thesis: ex j being Nat st
( k = (((k div l99) - 1) * ((len s2) - 1)) + j & 1 <= k div l99 & k div l99 <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
take l99 ; :: thesis: ( k = (((k div l99) - 1) * ((len s2) - 1)) + l99 & 1 <= k div l99 & k div l99 <= (len s1) - 1 & 1 <= l99 & l99 <= (len s2) - 1 )
thus k = (((k div l99) - 1) * ((len s2) - 1)) + l99 by A9, A10; :: thesis: ( 1 <= k div l99 & k div l99 <= (len s1) - 1 & 1 <= l99 & l99 <= (len s2) - 1 )
k div l99 > 0 by A1, A9, A10, FINSEQ_1:1;
then (k div l99) + 1 > 0 + 1 by XREAL_1:6;
hence 1 <= k div l99 by NAT_1:13; :: thesis: ( k div l99 <= (len s1) - 1 & 1 <= l99 & l99 <= (len s2) - 1 )
(k div l99) * l99 <= ((len s1) - 1) * l99 by A5, A6, A9, A10, INT_1:7;
then ((k div l99) * l99) / l99 <= (((len s1) - 1) * l99) / l99 by XREAL_1:72;
then k div l99 <= (((len s1) - 1) * l99) / l99 by A8, XCMPLX_1:89;
hence k div l99 <= (len s1) - 1 by A8, XCMPLX_1:89; :: thesis: ( 1 <= l99 & l99 <= (len s2) - 1 )
thus ( 1 <= l99 & l99 <= (len s2) - 1 ) by A7; :: thesis: verum
end;
suppose A11: k mod l99 <> 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 i = (k div l99) + 1;
set j = k mod l99;
take (k div l99) + 1 ; :: thesis: ex j being Nat st
( k = ((((k div l99) + 1) - 1) * ((len s2) - 1)) + j & 1 <= (k div l99) + 1 & (k div l99) + 1 <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
take k mod l99 ; :: thesis: ( k = ((((k div l99) + 1) - 1) * ((len s2) - 1)) + (k mod l99) & 1 <= (k div l99) + 1 & (k div l99) + 1 <= (len s1) - 1 & 1 <= k mod l99 & k mod l99 <= (len s2) - 1 )
thus k = ((((k div l99) + 1) - 1) * ((len s2) - 1)) + (k mod l99) by A8, NAT_D:2; :: thesis: ( 1 <= (k div l99) + 1 & (k div l99) + 1 <= (len s1) - 1 & 1 <= k mod l99 & k mod l99 <= (len s2) - 1 )
0 + 1 <= (k div l99) + 1 by XREAL_1:6;
hence 1 <= (k div l99) + 1 ; :: thesis: ( (k div l99) + 1 <= (len s1) - 1 & 1 <= k mod l99 & k mod l99 <= (len s2) - 1 )
k + 1 <= l by A6, INT_1:7;
then A12: (k + 1) - 1 <= l - 1 by XREAL_1:9;
(k mod l99) + (l99 * (k div l99)) >= 0 + (l99 * (k div l99)) by XREAL_1:6;
then A13: (k div l99) * l99 <= k by A8, NAT_D:2;
k <> l9 * l99 by A11, NAT_D:13;
then k < ((len s1) - 1) * l99 by A5, A12, XXREAL_0:1;
then (k div l99) * l99 < ((len s1) - 1) * l99 by A13, XXREAL_0:2;
then ((k div l99) * l99) / l99 < (((len s1) - 1) * l99) / l99 by A8, XREAL_1:74;
then k div l99 < (((len s1) - 1) * l99) / l99 by A8, XCMPLX_1:89;
then k div l99 < (len s1) - 1 by A8, XCMPLX_1:89;
hence (k div l99) + 1 <= (len s1) - 1 by INT_1:7; :: thesis: ( 1 <= k mod l99 & k mod l99 <= (len s2) - 1 )
(k mod l99) + 1 > 0 + 1 by A11, XREAL_1:6;
hence 1 <= k mod l99 by NAT_1:13; :: thesis: k mod l99 <= (len s2) - 1
thus k mod l99 <= (len s2) - 1 by A8, NAT_D:1; :: thesis: verum
end;
end;