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

1 = 2 - 1 ;
then (len g) - 1 >= 1 by A2, XREAL_1:11;
then A5: (len g) - 1 > 0 by XXREAL_0:2;
assume not f is s.n.c. ; :: thesis: contradiction
then consider i, j being Nat such that
A6: i + 1 < j and
A7: not LSeg f,i misses LSeg f,j by TOPREAL1:def 9;
A8: j in NAT by ORDINAL1:def 13;

A9: now

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

end;

then j < len f by NAT_1:13;
then A10: LSeg (f ^' g),j = LSeg f,j by A8, TOPREAL8:28;
(len (f ^' g)) + 1 = (len f) + (len g) by A3, GRAPH_2:13;
then ((len (f ^' g)) + 1) - 1 = (len f) + ((len g) - 1) ;
then len f < len (f ^' g) by A5, XREAL_1:31;
then A11: j + 1 < len (f ^' g) by A9, XXREAL_0:2;
A12: i in NAT by ORDINAL1:def 13;

now

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

end;

then i < len f by NAT_1:13;
then LSeg (f ^' g),i = LSeg f,i by A12, TOPREAL8:28;
hence contradiction by A1, A6, A7, A11, A12, A8, A10, GOBOARD5:def 4; :: thesis: verum

end;

now

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

end;

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