let i1, j1, i2, j2 be Element of NAT ; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds
cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))
let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) implies cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1)) )
assume that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: [i2,j2] in Indices G2 and
A4: G1 * (i1,j1) = G2 * (i2,j2) ; :: thesis: cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))
A5: 1 <= i1 by A2, MATRIX_1:39;
A6: 1 <= j2 by A3, MATRIX_1:39;
A7: 1 <= i2 by A3, MATRIX_1:39;
A8: j1 <= width G1 by A2, MATRIX_1:39;
A9: j2 <= width G2 by A3, MATRIX_1:39;
A10: i2 <= len G2 by A3, MATRIX_1:39;
then A11: (G2 * (i2,j2)) `1 = (G2 * (i2,1)) `1 by A7, A6, A9, GOBOARD5:3;
A12: i1 <= len G1 by A2, MATRIX_1:39;
A13: 1 <= j1 by A2, MATRIX_1:39;
then A15: (G1 * (i1,j1)) `2 = (G1 * (1,j1)) `2 by A5, A12, A8, GOBOARD5:2;
let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in cell (G2,i2,(j2 -' 1)) or p in cell (G1,i1,(j1 -' 1)) )
assume A16: p in cell (G2,i2,(j2 -' 1)) ; :: thesis: p in cell (G1,i1,(j1 -' 1))
A17: (G2 * (i2,j2)) `2 = (G2 * (1,j2)) `2 by A7, A10, A6, A9, GOBOARD5:2;

per cases ( ( j1 = 1 & j2 = 1 ) or ( j1 = 1 & 1 < j2 ) or ( 1 < j1 & j2 = 1 ) or ( 1 < j1 & 1 < j2 ) ) by A13, A6, XXREAL_0:1;

suppose A18: ( j1 = 1 & j2 = 1 ) ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then A19: j1 -' 1 = 0 by XREAL_1:234;
A20: j2 -' 1 = 0 by A18, XREAL_1:234;

now

per cases ( i2 = len G2 or i2 < len G2 ) by A10, XXREAL_0:1;

suppose A21: i2 = len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * ((len G2),1)) `1 <= r & s <= (G2 * (1,1)) `2 ) } by A16, A20, GOBRD11:27;
then consider r9, s9 being Real such that
A22: ( p = |[r9,s9]| & (G2 * ((len G2),1)) `1 <= r9 ) and
A23: s9 <= (G2 * (1,1)) `2 ;
A24: i1 = len G1 by A1, A2, A4, A6, A9, A21, Th11;
(G2 * (1,1)) `2 = (G2 * (i2,j2)) `2 by A7, A10, A9, A18, GOBOARD5:2;
then s9 <= (G1 * (1,1)) `2 by A4, A5, A12, A8, A18, A23, GOBOARD5:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * ((len G1),1)) `1 <= r & s <= (G1 * (1,1)) `2 ) } by A4, A18, A21, A22, A24;
hence p in cell (G1,i1,(j1 -' 1)) by A19, A24, GOBRD11:27; :: thesis: verum

end;

suppose A25: i2 < len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & s <= (G2 * (1,1)) `2 ) } by A16, A7, A20, GOBRD11:30;
then consider r9, s9 being Real such that
A26: ( p = |[r9,s9]| & (G2 * (i2,1)) `1 <= r9 ) and
A27: r9 <= (G2 * ((i2 + 1),1)) `1 and
A28: s9 <= (G2 * (1,1)) `2 ;
(G2 * (1,1)) `2 = (G2 * (i2,j1)) `2 by A7, A10, A9, A18, GOBOARD5:2;
then A29: s9 <= (G1 * (1,1)) `2 by A4, A5, A12, A8, A18, A28, GOBOARD5:2;

now

per cases ( i1 = len G1 or i1 < len G1 ) by A12, XXREAL_0:1;

suppose A30: i1 = len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G1 * ((len G1),1)) `1 <= r & s <= (G1 * (1,1)) `2 ) } by A4, A18, A26, A29;
hence p in cell (G1,i1,(j1 -' 1)) by A19, A30, GOBRD11:27; :: thesis: verum

end;

suppose A31: i1 < len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then (G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A8, A7, A9, A18, A25, Th14;
then r9 <= (G1 * ((i1 + 1),1)) `1 by A27, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & s <= (G1 * (1,1)) `2 ) } by A4, A18, A26, A29;
hence p in cell (G1,i1,(j1 -' 1)) by A5, A19, A31, GOBRD11:30; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

suppose that A32: j1 = 1 and
A33: 1 < j2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

A34: j1 -' 1 = 0 by A32, XREAL_1:234;
A35: 1 <= j2 -' 1 by A33, NAT_D:49;
then j2 -' 1 < j2 by NAT_D:51;
then A36: j2 -' 1 < width G2 by A9, XXREAL_0:2;
A37: (j2 -' 1) + 1 = j2 by A33, XREAL_1:237;

now

per cases ( i2 = len G2 or i2 < len G2 ) by A10, XXREAL_0:1;

suppose A38: i2 = len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) } by A16, A35, A36, A37, GOBRD11:29;
then ex r9, s9 being Real st
( p = |[r9,s9]| & (G2 * (i2,1)) `1 <= r9 & (G2 * (1,(j2 -' 1))) `2 <= s9 & s9 <= (G2 * (1,j2)) `2 ) ;
then A39: p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & s <= (G1 * (1,1)) `2 ) } by A4, A15, A11, A17, A32;
i1 = len G1 by A1, A2, A4, A6, A9, A38, Th11;
hence p in cell (G1,i1,(j1 -' 1)) by A34, A39, GOBRD11:27; :: thesis: verum

end;

suppose A40: i2 < len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) } by A16, A7, A35, A36, A37, GOBRD11:32;
then consider r9, s9 being Real such that
A41: p = |[r9,s9]| and
A42: (G2 * (i2,1)) `1 <= r9 and
A43: r9 <= (G2 * ((i2 + 1),1)) `1 and
(G2 * (1,(j2 -' 1))) `2 <= s9 and
A44: s9 <= (G2 * (1,j2)) `2 ;
A45: ( s9 <= (G1 * (1,1)) `2 & (G1 * (i1,1)) `1 <= r9 ) by A4, A7, A10, A6, A9, A15, A32, A42, A44, GOBOARD5:2, GOBOARD5:3;

now

per cases ( i1 = len G1 or i1 < len G1 ) by A12, XXREAL_0:1;

suppose A46: i1 = len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G1 * ((len G1),1)) `1 <= r & s <= (G1 * (1,1)) `2 ) } by A41, A45;
hence p in cell (G1,i1,(j1 -' 1)) by A34, A46, GOBRD11:27; :: thesis: verum

end;

suppose A47: i1 < len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A40, NAT_1:12, NAT_1:13;
then A48: (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by A6, A9, GOBOARD5:3;
( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by A47, NAT_1:12, NAT_1:13;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by A13, A8, GOBOARD5:3;
then (G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A7, A6, A9, A40, A47, A48, Th14;
then r9 <= (G1 * ((i1 + 1),1)) `1 by A43, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & s <= (G1 * (1,1)) `2 ) } by A41, A45;
hence p in cell (G1,i1,(j1 -' 1)) by A5, A34, A47, GOBRD11:30; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

suppose ( 1 < j1 & j2 = 1 ) ; :: thesis: p in cell (G1,i1,(j1 -' 1))

hence p in cell (G1,i1,(j1 -' 1)) by A1, A2, A4, A7, A10, Th12; :: thesis: verum

end;

suppose A49: ( 1 < j1 & 1 < j2 ) ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then A50: 1 <= j2 -' 1 by NAT_D:49;
then A51: (j2 -' 1) + 1 = j2 by NAT_D:43;
j2 -' 1 < j2 by A50, NAT_D:51;
then A52: j2 -' 1 < width G2 by A9, XXREAL_0:2;
then A53: (G2 * (1,(j2 -' 1))) `2 = (G2 * (i2,(j2 -' 1))) `2 by A7, A10, A50, GOBOARD5:2;
A54: 1 <= j1 -' 1 by A49, NAT_D:49;
then A55: (j1 -' 1) + 1 = j1 by NAT_D:43;
j1 -' 1 < j1 by A54, NAT_D:51;
then A56: j1 -' 1 < width G1 by A8, XXREAL_0:2;
then (G1 * (1,(j1 -' 1))) `2 = (G1 * (i1,(j1 -' 1))) `2 by A5, A12, A54, GOBOARD5:2;
then A57: (G1 * (1,(j1 -' 1))) `2 <= (G2 * (1,(j2 -' 1))) `2 by A1, A4, A5, A12, A8, A7, A10, A9, A49, A53, Th17;

now

per cases ( i2 = len G2 or i2 < len G2 ) by A10, XXREAL_0:1;

suppose A58: i2 = len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) } by A16, A50, A52, A51, GOBRD11:29;
then consider r9, s9 being Real such that
A59: p = |[r9,s9]| and
A60: (G2 * (i2,1)) `1 <= r9 and
A61: ( (G2 * (1,(j2 -' 1))) `2 <= s9 & s9 <= (G2 * (1,j2)) `2 ) ;
A62: (G1 * (i1,1)) `1 <= r9 by A4, A5, A12, A13, A8, A11, A60, GOBOARD5:3;
( (G1 * (1,(j1 -' 1))) `2 <= s9 & s9 <= (G1 * (1,j1)) `2 ) by A4, A5, A12, A13, A8, A17, A57, A61, GOBOARD5:2, XXREAL_0:2;
then A63: p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) } by A59, A62;
i1 = len G1 by A1, A2, A4, A6, A9, A58, Th11;
hence p in cell (G1,i1,(j1 -' 1)) by A54, A56, A55, A63, GOBRD11:29; :: thesis: verum

end;

suppose A64: i2 < len G2 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) } by A16, A7, A50, A52, A51, GOBRD11:32;
then consider r9, s9 being Real such that
A65: p = |[r9,s9]| and
A66: (G2 * (i2,1)) `1 <= r9 and
A67: r9 <= (G2 * ((i2 + 1),1)) `1 and
A68: ( (G2 * (1,(j2 -' 1))) `2 <= s9 & s9 <= (G2 * (1,j2)) `2 ) ;
A69: (G1 * (i1,1)) `1 <= r9 by A4, A5, A12, A13, A8, A11, A66, GOBOARD5:3;
A70: ( (G1 * (1,(j1 -' 1))) `2 <= s9 & s9 <= (G1 * (1,j1)) `2 ) by A4, A5, A12, A13, A8, A17, A57, A68, GOBOARD5:2, XXREAL_0:2;

now

per cases ( i1 = len G1 or i1 < len G1 ) by A12, XXREAL_0:1;

suppose A71: i1 = len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) } by A65, A70, A69;
hence p in cell (G1,i1,(j1 -' 1)) by A54, A56, A55, A71, GOBRD11:29; :: thesis: verum

end;

suppose A72: i1 < len G1 ; :: thesis: p in cell (G1,i1,(j1 -' 1))

( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A64, NAT_1:12, NAT_1:13;
then A73: (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by A6, A9, GOBOARD5:3;
( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by A72, NAT_1:12, NAT_1:13;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by A13, A8, GOBOARD5:3;
then (G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A7, A6, A9, A64, A72, A73, Th14;
then r9 <= (G1 * ((i1 + 1),1)) `1 by A67, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) } by A65, A70, A69;
hence p in cell (G1,i1,(j1 -' 1)) by A5, A54, A56, A55, A72, GOBRD11:32; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

end;

end;

hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum

end;

end;