theorem LMStat2: :: AESCIP_1:17

for k, i, j, i0, j0 being Nat st 1 <= k & k <= 128 & i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= ((1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32)) + 7 holds
( i = i0 & j = j0 )