let O be set ; 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; 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; 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; ( 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
; ( 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
; ( 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
; 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
;
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
;
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
;
( 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;
( 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;
( 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;
( 1 <= l99 & l99 <= (len s2) - 1 )thus
( 1
<= l99 &
l99 <= (len s2) - 1 )
by A7;
verum end; suppose A11:
k mod l99 <> 0
;
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
;
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
;
( 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;
( 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
;
( (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;
( 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;
k mod l99 <= (len s2) - 1thus
k mod l99 <= (len s2) - 1
by A8, NAT_D:1;
verum end; end;