let k, i, j, i0, j0 be Nat; :: thesis: ( 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 implies ( i = i0 & j = j0 ) )
assume AS: ( 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 ) ; :: thesis: ( i = i0 & j = j0 )
assume ( not i = i0 or not j = j0 ) ; :: thesis: contradiction
then A2: { n where n is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= n & n <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } /\ { n where n is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= n & n <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } = {} by LMStat2A, AS;
A3: k in { n where n is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= n & n <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } by AS;
k in { n where n is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= n & n <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } by AS;
hence contradiction by A3, XBOOLE_0:def 4, A2; :: thesis: verum