let O be set ; for G being GroupWithOperators of O
for k being Integer
for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
let G be GroupWithOperators of O; for k being Integer
for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
let k be Integer; for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
let i, j be Nat; for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
let s1, s2 be CompositionSeries of G; ( len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 implies ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) ) )
set l9 = (len s1) - 1;
set l99 = (len s2) - 1;
assume
len s2 > 1
; ( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 or ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) ) )
then A1:
(len s2) - 1 > 1 - 1
by XREAL_1:9;
assume A2:
k = ((i - 1) * ((len s2) - 1)) + j
; ( not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 or ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) ) )
assume that
A3:
1 <= i
and
A4:
i <= (len s1) - 1
; ( not 1 <= j or not j <= (len s2) - 1 or ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) ) )
assume that
A5:
1 <= j
and
A6:
j <= (len s2) - 1
; ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
i - 1 <= ((len s1) - 1) - 1
by A4, XREAL_1:9;
then
(i - 1) * ((len s2) - 1) <= (((len s1) - 1) - 1) * ((len s2) - 1)
by A1, XREAL_1:64;
then A7:
k <= ((((len s1) - 1) * ((len s2) - 1)) - (1 * ((len s2) - 1))) + ((len s2) - 1)
by A2, A6, XREAL_1:7;
1 - 1 <= i - 1
by A3, XREAL_1:9;
then
0 + 1 <= ((i - 1) * ((len s2) - 1)) + j
by A5, A1, XREAL_1:7;
hence
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
by A2, A7; verum