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 <> 0 by A2, CARD_1:27;

A4: now :: thesis: f is s.n.c.

1 = 2 - 1 ;
then (len g) - 1 >= 1 by A2, XREAL_1:9;
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) ;

A8: now :: thesis: ( 1 <= j & j + 1 <= len f )

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

end;

then j < len f by NAT_1:13;
then A9: LSeg ((f ^' g),j) = LSeg (f,j) by TOPREAL8:28;
(len (f ^' g)) + 1 = (len f) + (len g) by A3, FINSEQ_6:139;
then ((len (f ^' g)) + 1) - 1 = (len f) + ((len g) - 1) ;
then len f < len (f ^' g) by A5, XREAL_1:29;
then A10: j + 1 < len (f ^' g) by A8, XXREAL_0:2;

now :: thesis: ( 1 <= i & i + 1 <= len f )

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

end;

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

end;

now :: thesis: f is unfolded

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

end;

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