:: Properties of Go-Board - Part III
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

Lm1: now__::_thesis:_for_f_being_FinSequence_of_(TOP-REAL_2)
for_k_being_Element_of_NAT_st_len_f_=_k_+_1_&amp;_k_<>_0_&amp;_f_is_unfolded_holds_
f_|_k_is_unfolded
let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st len f = k + 1 &amp; k <> 0 &amp; f is unfolded holds
f | k is unfolded
let k be Element of NAT ; ::_thesis: ( len f = k + 1 &amp; k <> 0 &amp; f is unfolded implies f | k is unfolded )
A1: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def_3;
assume A2: len f = k + 1 ; ::_thesis: ( k <> 0 &amp; f is unfolded implies f | k is unfolded )
then A3: len (f | k) = k by FINSEQ_1:59, NAT_1:11;
assume  k <> 0 ; ::_thesis: ( f is unfolded implies f | k is unfolded )
then A4: 0 + 1 <= k by NAT_1:13;
assume A5: f is unfolded ; ::_thesis: f | k is unfolded
A6: k <= k + 1 by NAT_1:11;
then A7: k in dom f by A2, A4, FINSEQ_3:25;
thus  f | k is unfolded ::_thesis: verum
proof
let n be Nat; :: according toTOPREAL1:def_6 ::_thesis: ( not 1 <= n or not n + 2 <= len (f | k) or (LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))} )
set f1 = f | k;
assume that
A8: 1 <= n and
A9: n + 2 <= len (f | k) ; ::_thesis: (LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))}
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A10: n + 1 in dom (f | k) by A8, A9, SEQ_4:135;
 n in dom (f | k) by A8, A9, SEQ_4:135;
then A11: LSeg ((f | k),n) = LSeg (f,n) by A10, TOPREAL3:17;
 len (f | k) <= len f by A2, A6, FINSEQ_1:59;
then A12: n + 2 <= len f by A9, XXREAL_0:2;
A13: (n + 1) + 1 = n + (1 + 1) ;
 n + 2 in dom (f | k) by A8, A9, SEQ_4:135;
then A14: LSeg ((f | k),(n + 1)) = LSeg (f,(n + 1)) by A10, A13, TOPREAL3:17;
 (f | k) /. (n + 1) = f /. (n + 1) by A7, A3, A1, A10, FINSEQ_4:71;
hence  (LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))} by A5, A8, A11, A14, A12, TOPREAL1:def_6; ::_thesis: verum
end;
end;

theorem Th1: :: GOBOARD3:1
for f being FinSequence of (TOP-REAL 2)
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 &amp; f /. n = G * (i,j) ) ) &amp; f is one-to-one &amp; f is unfolded &amp; f is s.n.c. &amp; f is special holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G &amp; g is one-to-one &amp; g is unfolded &amp; g is s.n.c. &amp; g is special &amp; L~ f = L~ g &amp; f /. 1 = g /. 1 &amp; f /. (len f) = g /. (len g) &amp; len f <= len g )
proofend;

theorem :: GOBOARD3:2
for f being FinSequence of (TOP-REAL 2)
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 &amp; f /. n = G * (i,j) ) ) &amp; f is being_S-Seq holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G &amp; g is being_S-Seq &amp; L~ f = L~ g &amp; f /. 1 = g /. 1 &amp; f /. (len f) = g /. (len g) &amp; len f <= len g )
proofend;