let G be Go-board; 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); ( 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
; 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
; SEQM_3:def 10 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; verum