let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st ( for n being Nat st n in dom f holds
ex i, j being 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 Nat st n in dom f holds
ex i, j being 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 Nat st n in dom f holds
ex i, j being 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 )
( f is one-to-one & f is unfolded & f is s.n.c. & f is special ) by A2;
then consider g being FinSequence of (TOP-REAL 2) such that
A3: g is_sequence_on G and
A4: ( g is one-to-one & g is unfolded & g is s.n.c. & g is special ) and
A5: ( L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) ) and
A6: 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 A3; :: 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 f by A2;
then 2 <= len g by A6, XXREAL_0:2;
hence g is being_S-Seq by A4; :: 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, A6; :: thesis: verum