let G be Go-board; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds
not f is constant
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 & f is_sequence_on G implies not f is constant )
assume that
A1: len f >= 2 and
A2: f is_sequence_on G ; :: thesis: not f is constant
assume A3: for n, m being Nat st n in dom f & m in dom f holds
f . n = f . m ; :: according to SEQM_3:def 10 :: thesis: contradiction
1 <= len f by A1, XXREAL_0:2;
then A4: 1 in dom f by FINSEQ_3:25;
then consider i1, j1 being Nat such that
A5: [i1,j1] in Indices G and
A6: f /. 1 = G * (i1,j1) by A2;
A7: 1 + 1 in dom f by A1, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A8: [i2,j2] in Indices G and
A9: f /. 2 = G * (i2,j2) by A2;
A10: f /. 1 = f . 1 by A4, PARTFUN1:def 6
.= f . 2 by A3, A4, A7
.= f /. 2 by A7, PARTFUN1:def 6 ;
then A11: i1 = i2 by A5, A6, A8, A9, GOBOARD1:5;
A12: j1 = j2 by A5, A6, A8, A9, A10, GOBOARD1:5;
A13: |.(i1 - i2).| = 0 by A11, ABSVALUE:2;
|.(i1 - i2).| + |.(j1 - j2).| = 1 by A2, A4, A5, A6, A7, A8, A9;
hence contradiction by A12, A13; :: thesis: verum