let i, n, j be Element of NAT ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies ( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) ) )
assume A1: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: ( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) )
set m3 = ((2 * n) + (n * i)) + j;
A2: (2 * n) + n = (2 + 1) * n ;
n * 1 <= n * i by A1, XREAL_1:66;
then (2 * n) + n <= (2 * n) + (n * i) by XREAL_1:9;
hence (3 * n) + 1 <= ((2 * n) + (n * i)) + j by A1, XREAL_1:9; :: thesis: ((2 * n) + (n * i)) + j <= (n * n) + (3 * n)
A3: (2 * n) + j <= 3 * n by A1, A2, XREAL_1:9;
A4: ((2 * n) + (n * i)) + j = ((2 * n) + j) + (n * i) ;
n * i <= n * n by A1, XREAL_1:66;
hence ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) by A3, A4, XREAL_1:9; :: thesis: verum