let i, j, i0, j0 be Nat; :: thesis: ( 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 ) ) ; :: thesis: { 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;

per cases ( j <> j0 or j = j0 ) ;

suppose A2: j <> j0 ; :: thesis: { 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) ) } = {}

now :: thesis: { 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) ) } = {}

per cases ( j < j0 or j0 < j ) by A2, XXREAL_0:1;

suppose j < j0 ; :: thesis: { 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) ) } = {}

then j -' 1 < j0 -' 1 by XREAL_1:14, P1, P3;
then (j -' 1) + 1 <= j0 -' 1 by NAT_1:13;
then A12: ((j -' 1) + 1) * 32 <= (j0 -' 1) * 32 by XREAL_1:64;
(i -' 1) * 8 <= 3 * 8 by R2, XREAL_1:64;
then 8 + ((i -' 1) * 8) <= 8 + 24 by XREAL_1:6;
then (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= 32 + ((j -' 1) * 32) by XREAL_1:6;
then A13: (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= (j0 -' 1) * 32 by A12, XXREAL_0:2;
0 + ((j0 -' 1) * 32) <= ((i0 -' 1) * 8) + ((j0 -' 1) * 32) by XREAL_1:6;
then ((j0 -' 1) * 32) + 0 < (((i0 -' 1) * 8) + ((j0 -' 1) * 32)) + 1 by XREAL_1:8;
then A14: (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) < (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) by A13, XXREAL_0:2;
thus { 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) ) } = {} :: thesis: verum

proof

assume { 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) ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A150: x in { 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) ) } by XBOOLE_0:def 1;
A15: ( x in { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } & x in { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } ) by XBOOLE_0:def 4, A150;
consider k1 being Nat such that
A16: ( x = k1 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k1 & k1 <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) by A15;
consider k2 being Nat such that
A17: ( x = k2 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k2 & k2 <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) by A15;
reconsider x = x as Nat by A16;
thus contradiction by A17, A14, XXREAL_0:2, A16; :: thesis: verum

end;

end;

suppose j0 < j ; :: thesis: { 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) ) } = {}

then j0 -' 1 < j -' 1 by XREAL_1:14, P1, P3;
then (j0 -' 1) + 1 <= j -' 1 by NAT_1:13;
then A12: ((j0 -' 1) + 1) * 32 <= (j -' 1) * 32 by XREAL_1:64;
(i0 -' 1) * 8 <= 3 * 8 by R4, XREAL_1:64;
then 8 + ((i0 -' 1) * 8) <= 8 + 24 by XREAL_1:6;
then (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= 32 + ((j0 -' 1) * 32) by XREAL_1:6;
then A13: (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= (j -' 1) * 32 by A12, XXREAL_0:2;
0 + ((j -' 1) * 32) <= ((i -' 1) * 8) + ((j -' 1) * 32) by XREAL_1:6;
then ((j -' 1) * 32) + 0 < (((i -' 1) * 8) + ((j -' 1) * 32)) + 1 by XREAL_1:8;
then A14: (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) < (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) by A13, XXREAL_0:2;
thus { 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) ) } = {} :: thesis: verum

proof

assume { 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) ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A150: x in { 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) ) } by XBOOLE_0:def 1;
A15: ( x in { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } & x in { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } ) by XBOOLE_0:def 4, A150;
consider k1 being Nat such that
A16: ( x = k1 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k1 & k1 <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) by A15;
consider k2 being Nat such that
A17: ( x = k2 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k2 & k2 <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) by A15;
reconsider x = x as Nat by A16;
thus contradiction by A16, A14, XXREAL_0:2, A17; :: thesis: verum

end;

end;

end;

end;

hence { 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) ) } = {} ; :: thesis: verum

end;

suppose A2: j = j0 ; :: thesis: { 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) ) } = {}

now :: thesis: { 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) ) } = {}

per cases ( i < i0 or i0 < i ) by A2, AS, XXREAL_0:1;

suppose i < i0 ; :: thesis: { 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) ) } = {}

then i -' 1 < i0 -' 1 by XREAL_1:14, P2, P4;
then (i -' 1) + 1 <= i0 -' 1 by NAT_1:13;
then ((i -' 1) + 1) * 8 <= (i0 -' 1) * 8 by XREAL_1:64;
then A13: (((i -' 1) * 8) + 8) + ((j -' 1) * 32) <= ((i0 -' 1) * 8) + ((j0 -' 1) * 32) by A2, XREAL_1:6;
(((i0 -' 1) * 8) + ((j0 -' 1) * 32)) + 0 < (((i0 -' 1) * 8) + ((j0 -' 1) * 32)) + 1 by XREAL_1:8;
then A14: (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) < (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) by A13, XXREAL_0:2;
thus { 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) ) } = {} :: thesis: verum

proof

assume { 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) ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A150: x in { 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) ) } by XBOOLE_0:def 1;
A15: ( x in { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } & x in { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } ) by XBOOLE_0:def 4, A150;
consider k1 being Nat such that
A16: ( x = k1 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k1 & k1 <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) by A15;
consider k2 being Nat such that
A17: ( x = k2 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k2 & k2 <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) by A15;
reconsider x = x as Nat by A16;
thus contradiction by A16, A17, A14, XXREAL_0:2; :: thesis: verum

end;

end;

suppose i0 < i ; :: thesis: { 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) ) } = {}

then i0 -' 1 < i -' 1 by XREAL_1:14, P2, P4;
then (i0 -' 1) + 1 <= i -' 1 by NAT_1:13;
then ((i0 -' 1) + 1) * 8 <= (i -' 1) * 8 by XREAL_1:64;
then A13: (((i0 -' 1) * 8) + 8) + ((j0 -' 1) * 32) <= ((i -' 1) * 8) + ((j -' 1) * 32) by A2, XREAL_1:6;
(((i -' 1) * 8) + ((j -' 1) * 32)) + 0 < (((i -' 1) * 8) + ((j -' 1) * 32)) + 1 by XREAL_1:8;
then A14: (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) < (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) by A13, XXREAL_0:2;
thus { 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) ) } = {} :: thesis: verum

proof

assume { 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) ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A150: x in { 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) ) } by XBOOLE_0:def 1;
A15: ( x in { k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } & x in { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } ) by XBOOLE_0:def 4, A150;
consider k1 being Nat such that
A16: ( x = k1 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k1 & k1 <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) by A15;
consider k2 being Nat such that
A17: ( x = k2 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k2 & k2 <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) by A15;
reconsider x = x as Nat by A16;
thus contradiction by A16, A14, XXREAL_0:2, A17; :: thesis: verum

end;

end;

end;

end;

hence { 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) ) } = {} ; :: thesis: verum

end;

end;