let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f ^' g is unfolded & f ^' g is s.c.c. & len g >= 2 implies ( f is unfolded & f is s.n.c. ) )
assume that
A1: ( f ^' g is unfolded & f ^' g is s.c.c. ) and
A2: len g >= 2 ; :: thesis: ( f is unfolded & f is s.n.c. )
A3: g <> {} by A2, CARD_1:47;

A4: now

assume not f is s.n.c. ; :: thesis: contradiction
then consider i, j being Nat such that
A5: ( i + 1 < j & not LSeg f,i misses LSeg f,j ) by TOPREAL1:def 9;

now

assume ( not 1 <= i or not i + 1 <= len f ) ; :: thesis: contradiction
then LSeg f,i = {} by TOPREAL1:def 5;
hence contradiction by A5, XBOOLE_1:65; :: thesis: verum

end;

then A6: i < len f by NAT_1:13;

A7: now

assume ( not 1 <= j or not j + 1 <= len f ) ; :: thesis: contradiction
then LSeg f,j = {} by TOPREAL1:def 5;
hence contradiction by A5, XBOOLE_1:65; :: thesis: verum

end;

then A8: j < len f by NAT_1:13;
(len (f ^' g)) + 1 = (len f) + (len g) by A3, GRAPH_2:13;
then A9: ((len (f ^' g)) + 1) - 1 = (len f) + ((len g) - 1) ;
1 = 2 - 1 ;
then (len g) - 1 >= 1 by A2, XREAL_1:11;
then (len g) - 1 > 0 by XXREAL_0:2;
then len f < len (f ^' g) by A9, XREAL_1:31;
then A10: j + 1 < len (f ^' g) by A7, XXREAL_0:2;
A11: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
then A12: LSeg (f ^' g),i = LSeg f,i by A6, TOPREAL8:28;
LSeg (f ^' g),j = LSeg f,j by A8, A11, TOPREAL8:28;
hence contradiction by A1, A5, A10, A11, A12, GOBOARD5:def 4; :: thesis: verum

end;

now

assume not f is unfolded ; :: thesis: contradiction
then consider i being Nat such that
A13: ( 1 <= i & i + 2 <= len f & (LSeg f,i) /\ (LSeg f,(i + 1)) <> {(f /. (i + 1))} ) by TOPREAL1:def 8;
i + 1 < (i + 1) + 1 by NAT_1:13;
then A14: ( 1 <= i + 1 & i + 1 < len f ) by A13, NAT_1:13;
then A15: i + 1 in dom f by FINSEQ_3:27;
A16: len f <= len (f ^' g) by TOPREAL8:7;
then A17: i + 2 <= len (f ^' g) by A13, XXREAL_0:2;
i + 1 <= len (f ^' g) by A14, A16, XXREAL_0:2;
then A18: i + 1 in dom (f ^' g) by A14, FINSEQ_3:27;
A19: f /. (i + 1) = f . (i + 1) by A15, PARTFUN1:def 8
.= (f ^' g) . (i + 1) by A14, GRAPH_2:14
.= (f ^' g) /. (i + 1) by A18, PARTFUN1:def 8 ;
A20: i in NAT by ORDINAL1:def 13;
i < len f by A14, NAT_1:13;
then A21: LSeg (f ^' g),i = LSeg f,i by A20, TOPREAL8:28;
LSeg (f ^' g),(i + 1) = LSeg f,(i + 1) by A14, TOPREAL8:28;
hence contradiction by A1, A13, A17, A19, A21, TOPREAL1:def 8; :: thesis: verum

end;

hence ( f is unfolded & f is s.n.c. ) by A4; :: thesis: verum