let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
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: ( not f is constant & f is circular & f is unfolded ) and
A3: f is s.c.c. and
A4: f is special and
A5: len f > 4 ; :: thesis:
reconsider f' = f as non constant circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) by A2, A3, A4;
reconsider f' = f' as non constant non empty circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) ;
A6: len f > 1 + 1 by A2, Th3;
set h1 = f' | 2;
set h2 = f' /^ 1;
A7: len (f' | 2) = 1 + 1 by A6, FINSEQ_1:80;
then reconsider h1 = f' | 2 as non trivial FinSequence of (TOP-REAL 2) by REALSET1:13;
1 <= len f by A2, Th3, XXREAL_0:2;
then A8: len (f' /^ 1) = (len f) - 1 by RFINSEQ:def 2;
then A9: (len (f' /^ 1)) + 1 = len f ;
A10: len (f' /^ 1) > (1 + 1) - 1 by A6, A8, XREAL_1:11;
then A11: len (f' /^ 1) >= 2 by NAT_1:13;
then reconsider h2 = f' /^ 1 as non trivial FinSequence of (TOP-REAL 2) by REALSET1:13;
A12: (1 + 1),(len h2) -cut h2 = h2 /^ 1 by Th13;
A13: f = h1 ^ (f /^ (1 + 1)) by RFINSEQ:21
.= h1 ^ (2,(len h2) -cut h2) by A12, FINSEQ_6:87
.= h1 ^' h2 by GRAPH_2:def 2 ;
A14: dom h1 c= dom f by FINSEQ_5:20;
A15: for n being Element of NAT st n in dom h1 holds
ex i, j being Element of NAT st
( [i,j] in Indices G & h1 /. n = G * i,j )

proof

let n be Element of NAT ; :: thesis:
assume A16: n in dom h1 ; :: thesis:
then consider i, j being Nat such that
A17: [i,j] in Indices G and
A18: f /. n = G * i,j by A1, A14;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis:
take j ; :: thesis:
thus [i,j] in Indices G by A17; :: thesis:
thus h1 /. n = G * i,j by A16, A18, FINSEQ_4:85; :: thesis:

end;

A19: h1 is one-to-one by A5, Th3, Th22;
h1 is s.n.c. by A6, Th20;
then consider g1 being FinSequence of (TOP-REAL 2) such that
A20: g1 is_sequence_on G and
A21: ( g1 is one-to-one & g1 is unfolded & g1 is s.n.c. & g1 is special ) and
A22: L~ h1 = L~ g1 and
A23: h1 /. 1 = g1 /. 1 and
A24: h1 /. (len h1) = g1 /. (len g1) and
A25: len h1 <= len g1 by A15, A19, GOBOARD3:1;
reconsider g1 = g1 as non trivial FinSequence of (TOP-REAL 2) by A7, A25, REALSET1:13;
A26: for n being Element of NAT st n in dom h2 holds
ex i, j being Element of NAT st
( [i,j] in Indices G & h2 /. n = G * i,j )

proof

let n be Element of NAT ; :: thesis:
assume A27: n in dom h2 ; :: thesis:
then n + 1 in dom f by FINSEQ_5:29;
then consider i, j being Nat such that
A28: [i,j] in Indices G and
A29: f /. (n + 1) = G * i,j by A1;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis:
take j ; :: thesis:
thus [i,j] in Indices G by A28; :: thesis:
thus h2 /. n = G * i,j by A27, A29, FINSEQ_5:30; :: thesis:

end;

A30: h2 is one-to-one by A5, Th24;
h2 is s.n.c. by Th21;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A31: g2 is_sequence_on G and
A32: ( g2 is one-to-one & g2 is unfolded & g2 is s.n.c. & g2 is special ) and
A33: L~ h2 = L~ g2 and
A34: h2 /. 1 = g2 /. 1 and
A35: h2 /. (len h2) = g2 /. (len g2) and
A36: len h2 <= len g2 by A26, A30, GOBOARD3:1;
A37: len g2 >= 1 + 1 by A11, A36, XXREAL_0:2;
then reconsider g2 = g2 as non trivial FinSequence of (TOP-REAL 2) by REALSET1:13;
take g = g1 ^' g2; :: thesis:
A38: 1 in dom h2 by A10, FINSEQ_3:27;
A39: len h2 in dom h2 by FINSEQ_5:6;
len h1 in dom h1 by A7, FINSEQ_3:27;
then A40: h1 /. (len h1) = f /. (1 + 1) by A7, FINSEQ_4:85;
then A41: h1 /. (len h1) = h2 /. 1 by A38, FINSEQ_5:30;
A42: 1 in dom h1 by FINSEQ_5:6;
then A43: h1 /. 1 = f /. 1 by FINSEQ_4:85;
then A44: h1 /. 1 = f /. (len f) by FINSEQ_6:def 1
.= h2 /. (len h2) by A9, A39, FINSEQ_5:30 ;
thus g is_sequence_on G by A20, A24, A31, A34, A41, Th12; :: thesis:
A45: ((len g2) -' 1) + 1 = len g2 by A37, XREAL_1:237, XXREAL_0:2;
A46: ((len g1) -' 1) + 1 = len g1 by A7, A25, XREAL_1:237, XXREAL_0:2;
len h2 > (3 + 1) - 1 by A5, A8, XREAL_1:11;
then 2 + 1 < len g2 by A36, XXREAL_0:2;
then A47: 1 + 1 < (len g2) -' 1 by NAT_D:52;
(LSeg f,1) /\ (L~ h2) = {(h1 /. 1),(h2 /. 1)} by A5, A40, A41, A43, Th27;
then A48: (L~ g1) /\ (L~ g2) = {(g1 /. 1),(g2 /. 1)} by A22, A23, A33, A34, Th19;
1 <= (len g1) -' 1 by A7, A25, NAT_D:55;
then A49: g1 /. (len g1) in LSeg g1,((len g1) -' 1) by A46, TOPREAL1:27;
g2 /. 1 in LSeg g2,1 by A37, TOPREAL1:27;
then A50: g2 /. 1 in (LSeg g1,((len g1) -' 1)) /\ (LSeg g2,1) by A24, A34, A41, A49, XBOOLE_0:def 4;
A51: LSeg g2,1 misses LSeg g2,((len g2) -' 1) by A32, A47, TOPREAL1:def 9;
1 <= (len g2) -' 1 by A47, NAT_1:13;
then g2 /. (len g2) in LSeg g2,((len g2) -' 1) by A45, TOPREAL1:27;
then not g2 /. (len g2) in LSeg g2,1 by A51, XBOOLE_0:3;
then A52: not g2 /. (len g2) in (LSeg g1,((len g1) -' 1)) /\ (LSeg g2,1) by XBOOLE_0:def 4;
A53: LSeg g1,((len g1) -' 1) c= L~ g1 by TOPREAL3:26;
LSeg g2,1 c= L~ g2 by TOPREAL3:26;
then (LSeg g1,((len g1) -' 1)) /\ (LSeg g2,1) = {(g2 /. 1)} by A23, A35, A44, A48, A50, A52, A53, Th1, XBOOLE_1:27;
hence g is unfolded by A21, A24, A32, A34, A41, Th34; :: thesis:
thus g is s.c.c. by A21, A23, A24, A32, A34, A35, A41, A44, A48, Th33; :: thesis:
thus g is special by A21, A24, A32, A34, A41, Th26; :: thesis:
thus L~ f = (L~ h1) \/ (L~ h2) by A13, A41, Th35
.= L~ g by A22, A24, A33, A34, A41, Th35 ; :: thesis:
thus f /. 1 = h1 /. 1 by A42, FINSEQ_4:85
.= g /. 1 by A23, GRAPH_2:57 ; :: thesis:
thus f /. (len f) = h2 /. (len h2) by A9, A39, FINSEQ_5:30
.= g /. (len g) by A35, GRAPH_2:58 ; :: thesis:
A54: (len f) + 1 = (len h1) + (len h2) by A13, GRAPH_2:13;
(len g) + 1 = (len g1) + (len g2) by GRAPH_2:13;
then (len f) + 1 <= (len g) + 1 by A25, A36, A54, XREAL_1:9;
hence len f <= len g by XREAL_1:8; :: thesis: