let i1, j1, j2 be Nat; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) holds

i1 = len G1

let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) implies i1 = len G1 )

assume that

A1: Values G1 c= Values G2 and

A2: [i1,j1] in Indices G1 and

A3: ( 1 <= j2 & j2 <= width G2 ) and

A4: G1 * (i1,j1) = G2 * ((len G2),j2) ; :: thesis: i1 = len G1

set p = G1 * ((len G1),j1);

A5: ( 1 <= j1 & j1 <= width G1 ) by A2, MATRIX_0:32;

assume A6: i1 <> len G1 ; :: thesis: contradiction

i1 <= len G1 by A2, MATRIX_0:32;

then A7: i1 < len G1 by A6, XXREAL_0:1;

1 <= i1 by A2, MATRIX_0:32;

then A8: (G1 * (i1,j1)) `1 < (G1 * ((len G1),j1)) `1 by A5, A7, GOBOARD5:3;

0 <> len G1 by MATRIX_0:def 10;

then 1 <= len G1 by NAT_1:14;

then [(len G1),j1] in Indices G1 by A5, MATRIX_0:30;

then G1 * ((len G1),j1) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;

then G1 * ((len G1),j1) in Values G1 by MATRIX_0:39;

then G1 * ((len G1),j1) in Values G2 by A1;

then G1 * ((len G1),j1) 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 * ((len G1),j1) = G2 * (i,j) and

A10: [i,j] in Indices G2 ;

A11: ( 1 <= j & j <= width G2 ) by A10, MATRIX_0:32;

0 <> len G2 by MATRIX_0:def 10;

then A12: 1 <= len G2 by NAT_1:14;

then A13: (G2 * ((len G2),j)) `1 = (G2 * ((len G2),1)) `1 by A11, GOBOARD5:2

.= (G2 * ((len G2),j2)) `1 by A3, A12, GOBOARD5:2 ;

A14: 1 <= i by A10, MATRIX_0:32;

i <= len G2 by A10, MATRIX_0:32;

then i < len G2 by A4, A8, A9, A13, XXREAL_0:1;

hence contradiction by A4, A8, A9, A14, A11, A13, GOBOARD5:3; :: thesis: verum

i1 = len G1

let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) implies i1 = len G1 )

assume that

A1: Values G1 c= Values G2 and

A2: [i1,j1] in Indices G1 and

A3: ( 1 <= j2 & j2 <= width G2 ) and

A4: G1 * (i1,j1) = G2 * ((len G2),j2) ; :: thesis: i1 = len G1

set p = G1 * ((len G1),j1);

A5: ( 1 <= j1 & j1 <= width G1 ) by A2, MATRIX_0:32;

assume A6: i1 <> len G1 ; :: thesis: contradiction

i1 <= len G1 by A2, MATRIX_0:32;

then A7: i1 < len G1 by A6, XXREAL_0:1;

1 <= i1 by A2, MATRIX_0:32;

then A8: (G1 * (i1,j1)) `1 < (G1 * ((len G1),j1)) `1 by A5, A7, GOBOARD5:3;

0 <> len G1 by MATRIX_0:def 10;

then 1 <= len G1 by NAT_1:14;

then [(len G1),j1] in Indices G1 by A5, MATRIX_0:30;

then G1 * ((len G1),j1) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;

then G1 * ((len G1),j1) in Values G1 by MATRIX_0:39;

then G1 * ((len G1),j1) in Values G2 by A1;

then G1 * ((len G1),j1) 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 * ((len G1),j1) = G2 * (i,j) and

A10: [i,j] in Indices G2 ;

A11: ( 1 <= j & j <= width G2 ) by A10, MATRIX_0:32;

0 <> len G2 by MATRIX_0:def 10;

then A12: 1 <= len G2 by NAT_1:14;

then A13: (G2 * ((len G2),j)) `1 = (G2 * ((len G2),1)) `1 by A11, GOBOARD5:2

.= (G2 * ((len G2),j2)) `1 by A3, A12, GOBOARD5:2 ;

A14: 1 <= i by A10, MATRIX_0:32;

i <= len G2 by A10, MATRIX_0:32;

then i < len G2 by A4, A8, A9, A13, XXREAL_0:1;

hence contradiction by A4, A8, A9, A14, A11, A13, GOBOARD5:3; :: thesis: verum