theorem LMStat0: :: AESCIP_1:15

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