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;

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) ;

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;

then LSeg ((f ^' g),i) = LSeg (f,i) by TOPREAL8:28;

hence contradiction by A1, A6, A7, A10, A9; :: thesis: verum

end;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 )

then
j < len f
by NAT_1:13;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 LSeg (f,j) = {} by TOPREAL1:def 3;

hence contradiction by A7; :: thesis: verum

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 )

then
i < len f
by NAT_1:13;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 LSeg (f,i) = {} by TOPREAL1:def 3;

hence contradiction by A7; :: thesis: verum

then LSeg ((f ^' g),i) = LSeg (f,i) by TOPREAL8:28;

hence contradiction by A1, A6, A7, A10, A9; :: thesis: verum

now :: thesis: f is unfolded

hence
( f is unfolded & f is s.n.c. )
by A4; :: thesis: verumassume
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;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