let m, k, i, j be Element of NAT ; :: thesis: for x being set
for G being Go-board st x = G * m,k & x = G * i,j & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let x be set ; :: thesis: for G being Go-board st x = G * m,k & x = G * i,j & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let G be Go-board; :: thesis: ( x = G * m,k & x = G * i,j & [m,k] in Indices G & [i,j] in Indices G implies ( m = i & k = j ) )
assume that
A1: x = G * m,k and
A2: x = G * i,j and
A3: [m,k] in Indices G and
A4: [i,j] in Indices G ; :: thesis: ( m = i & k = j )
A5: ( len (Line G,m) = width G & dom (Line G,m) = Seg (len (Line G,m)) ) by FINSEQ_1:def 3, MATRIX_1:def 8;
A6: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A7: k in Seg (width G) by A3, ZFMISC_1:106;
then x = (Line G,m) . k by A1, MATRIX_1:def 8;
then A8: x in rng (Line G,m) by A7, A5, FUNCT_1:def 5;
A9: ( len (Col G,k) = len G & dom (Col G,k) = Seg (len (Col G,k)) ) by FINSEQ_1:def 3, MATRIX_1:def 9;
A10: ( len (Line G,i) = width G & dom (Line G,i) = Seg (len (Line G,i)) ) by FINSEQ_1:def 3, MATRIX_1:def 8;
A11: ( len (Col G,j) = len G & dom (Col G,j) = Seg (len (Col G,j)) ) by FINSEQ_1:def 3, MATRIX_1:def 9;
A12: dom G = Seg (len G) by FINSEQ_1:def 3;
A13: j in Seg (width G) by A4, A6, ZFMISC_1:106;
then x = (Line G,i) . j by A2, MATRIX_1:def 8;
then A14: x in rng (Line G,i) by A13, A10, FUNCT_1:def 5;
A15: i in dom G by A4, A6, ZFMISC_1:106;
then x = (Col G,j) . i by A2, MATRIX_1:def 9;
then A16: x in rng (Col G,j) by A15, A12, A11, FUNCT_1:def 5;
A17: m in dom G by A3, A6, ZFMISC_1:106;
then x = (Col G,k) . m by A1, MATRIX_1:def 9;
then x in rng (Col G,k) by A17, A12, A9, FUNCT_1:def 5;
hence ( m = i & k = j ) by A17, A15, A7, A13, A8, A14, A16, Th19, Th20; :: thesis: verum