let f be FinSequence of (TOP-REAL 2); :: thesis: for i, n, m, k being Element of NAT
for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let i, n, m, k be Element of NAT ; :: thesis: for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let G be Go-board; :: thesis: ( rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G implies i <> k )
assume that
A1: (rng f) /\ (rng (Col (G,i))) = {} and
A2: f /. n = G * (m,k) and
A3: n in dom f and
A4: m in dom G and
A5: i = k ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
f . n = G * (m,k) by A2, A3, PARTFUN1:def 6;
then A6: G * (m,i) in rng f by A3, A5, FUNCT_1:def 3;
A7: ( dom G = Seg (len G) & dom (Col (G,i)) = Seg (len (Col (G,i))) ) by FINSEQ_1:def 3;
( len (Col (G,i)) = len G & (Col (G,i)) . m = G * (m,i) ) by A4, MATRIX_1:def 8;
then G * (m,i) in rng (Col (G,i)) by A4, A7, FUNCT_1:def 3;
hence contradiction by A1, A6, XBOOLE_0:def 4; :: thesis: verum