let i1, i2, j1 be Nat; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,(width G2)) holds
j1 = width G1
let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,(width G2)) implies j1 = width G1 )
assume that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: ( 1 <= i2 & i2 <= len G2 ) and
A4: G1 * (i1,j1) = G2 * (i2,(width G2)) ; :: thesis: j1 = width G1
set p = G1 * (i1,(width G1));
A5: ( 1 <= i1 & i1 <= len G1 ) by A2, MATRIX_0:32;
assume A6: j1 <> width G1 ; :: thesis: contradiction
j1 <= width G1 by A2, MATRIX_0:32;
then A7: j1 < width G1 by A6, XXREAL_0:1;
1 <= j1 by A2, MATRIX_0:32;
then A8: (G1 * (i1,j1)) `2 < (G1 * (i1,(width G1))) `2 by A5, A7, GOBOARD5:4;
0 <> width G1 by MATRIX_0:def 10;
then 1 <= width G1 by NAT_1:14;
then [i1,(width G1)] in Indices G1 by A5, MATRIX_0:30;
then G1 * (i1,(width G1)) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;
then G1 * (i1,(width G1)) in Values G1 by MATRIX_0:39;
then G1 * (i1,(width G1)) in Values G2 by A1;
then G1 * (i1,(width G1)) in { (G2 * (i,j)) where i, j is Nat : [i,j] in Indices G2 } by MATRIX_0:39;
then consider i, j being Nat such that
A9: G1 * (i1,(width G1)) = G2 * (i,j) and
A10: [i,j] in Indices G2 ;
A11: ( 1 <= i & i <= len G2 ) by A10, MATRIX_0:32;
0 <> width G2 by MATRIX_0:def 10;
then A12: 1 <= width G2 by NAT_1:14;
then A13: (G2 * (i,(width G2))) `2 = (G2 * (1,(width G2))) `2 by A11, GOBOARD5:1
.= (G2 * (i2,(width G2))) `2 by A3, A12, GOBOARD5:1 ;
A14: 1 <= j by A10, MATRIX_0:32;
j <= width G2 by A10, MATRIX_0:32;
then j < width G2 by A4, A8, A9, A13, XXREAL_0:1;
hence contradiction by A4, A8, A9, A11, A14, A13, GOBOARD5:4; :: thesis: verum