let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) ) & f is being_S-Seq holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
let G be Go-board; :: thesis: ( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) ) & f is being_S-Seq implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) )
assume that
A1: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) and
A2: f is being_S-Seq ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
A3: ( f is one-to-one & 2 <= len f & f is unfolded & f is s.n.c. & f is special ) by A2, TOPREAL1:def 10;
then consider g being FinSequence of (TOP-REAL 2) such that
A4: g is_sequence_on G and
A5: ( g is one-to-one & g is unfolded & g is s.n.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) by A1, Th1;
take g ; :: thesis: ( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
thus g is_sequence_on G by A4; :: thesis: ( g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
2 <= len g by A3, A5, XXREAL_0:2;
hence g is being_S-Seq by A5, TOPREAL1:def 10; :: thesis: ( L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
thus ( L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) by A5; :: thesis: verum