let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum