let i1, j1, i2 be Element of 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,1 holds
j1 = 1
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,1 implies j1 = 1 )
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,1 ; :: thesis: j1 = 1
A5: ( 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 ) by A2, MATRIX_1:39;
0 <> width G2 by GOBOARD1:def 5;
then A6: 1 <= width G2 by NAT_1:14;
0 <> width G1 by GOBOARD1:def 5;
then A7: 1 <= width G1 by NAT_1:14;
set p = G1 * i1,1;
assume j1 <> 1 ; :: thesis: contradiction
then 1 < j1 by A5, XXREAL_0:1;
then A8: (G1 * i1,1) `2 < (G1 * i1,j1) `2 by A5, GOBOARD5:5;
[i1,1] in Indices G1 by A5, A7, MATRIX_1:37;
then G1 * i1,1 in { (G1 * i,j) where i, j is Element of NAT : [i,j] in Indices G1 } ;
then G1 * i1,1 in Values G1 by Th7;
then G1 * i1,1 in Values G2 by A1;
then G1 * i1,1 in { (G2 * i,j) where i, j is Element of NAT : [i,j] in Indices G2 } by Th7;
then consider i, j being Element of NAT such that
A9: G1 * i1,1 = G2 * i,j and
A10: [i,j] in Indices G2 ;
A11: ( 1 <= i & i <= len G2 & 1 <= j & j <= width G2 ) by A10, MATRIX_1:39;
then A12: (G2 * i,1) `2 = (G2 * 1,1) `2 by A6, GOBOARD5:2
.= (G2 * i2,1) `2 by A3, A6, GOBOARD5:2 ;
then 1 < j by A4, A8, A9, A11, XXREAL_0:1;
hence contradiction by A4, A8, A9, A11, A12, GOBOARD5:5; :: thesis: verum