let i, j, i0, j0 be Nat; ( i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & ( not i = i0 or not j = j0 ) implies { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } /\ { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } = {} )
assume AS:
( i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & ( not i = i0 or not j = j0 ) )
; { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } /\ { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } = {}
set A = { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } ;
set B = { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } ;
A1:
( 1 <= j & j <= 4 )
by AS, FINSEQ_1:1;
A2:
( 1 <= i & i <= 4 )
by AS, FINSEQ_1:1;
B1:
( 1 <= j0 & j0 <= 4 )
by AS, FINSEQ_1:1;
B2:
( 1 <= i0 & i0 <= 4 )
by AS, FINSEQ_1:1;
P1:
j -' 1 = j - 1
by XREAL_1:233, A1;
P2:
i -' 1 = i - 1
by XREAL_1:233, A2;
P3:
j0 -' 1 = j0 - 1
by XREAL_1:233, B1;
P4:
i0 -' 1 = i0 - 1
by XREAL_1:233, B2;
i - 1 <= 4 - 1
by A2, XREAL_1:9;
then R2:
i -' 1 <= 3
by XREAL_1:233, A2;
i0 - 1 <= 4 - 1
by B2, XREAL_1:9;
then R4:
i0 -' 1 <= 3
by XREAL_1:233, B2;