let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st i > 2 & i in dom f & f is being_S-Seq holds

f | i is being_S-Seq

let i be Nat; :: thesis: ( i > 2 & i in dom f & f is being_S-Seq implies f | i is being_S-Seq )

assume that

A1: i > 2 and

A2: i in dom f and

A3: f is being_S-Seq ; :: thesis: f | i is being_S-Seq

A4: f | i = f | (Seg i) by FINSEQ_1:def 15;

then A5: dom (f | i) = (dom f) /\ (Seg i) by RELAT_1:61;

thus f | i is one-to-one :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len (f | i) & f | i is unfolded & f | i is s.n.c. & f | i is special )

A12: i in NAT by ORDINAL1:def 12;

Seg (len f) = dom f by FINSEQ_1:def 3;

then Seg i c= dom f by A11, FINSEQ_1:5;

then A13: dom (f | i) = Seg i by A5, XBOOLE_1:28;

hence len (f | i) >= 2 by A1, A12, FINSEQ_1:def 3; :: thesis: ( f | i is unfolded & f | i is s.n.c. & f | i is special )

A14: f is unfolded by A3;

thus f | i is unfolded :: thesis: ( f | i is s.n.c. & f | i is special )

thus f | i is s.n.c. :: thesis: f | i is special

assume that

A30: 1 <= j and

A31: j + 1 <= len (f | i) ; :: thesis: ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 )

len (f | i) <= len f by A11, A13, A12, FINSEQ_1:def 3;

then A32: j + 1 <= len f by A31, XXREAL_0:2;

j <= j + 1 by NAT_1:11;

then j <= len (f | i) by A31, XXREAL_0:2;

then j in dom (f | i) by A30, FINSEQ_3:25;

then A33: (f | i) /. j = f /. j by FINSEQ_4:70;

1 <= j + 1 by NAT_1:12;

then j + 1 in dom (f | i) by A31, FINSEQ_3:25;

then A34: (f | i) /. (j + 1) = f /. (j + 1) by FINSEQ_4:70;

f is special by A3;

hence ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 ) by A30, A32, A33, A34; :: thesis: verum

f | i is being_S-Seq

let i be Nat; :: thesis: ( i > 2 & i in dom f & f is being_S-Seq implies f | i is being_S-Seq )

assume that

A1: i > 2 and

A2: i in dom f and

A3: f is being_S-Seq ; :: thesis: f | i is being_S-Seq

A4: f | i = f | (Seg i) by FINSEQ_1:def 15;

then A5: dom (f | i) = (dom f) /\ (Seg i) by RELAT_1:61;

thus f | i is one-to-one :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len (f | i) & f | i is unfolded & f | i is s.n.c. & f | i is special )

proof

A11:
i <= len f
by A2, FINSEQ_3:25;
A6:
f is one-to-one
by A3;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (f | i) or not y in dom (f | i) or not (f | i) . x = (f | i) . y or x = y )

assume that

A7: x in dom (f | i) and

A8: y in dom (f | i) and

A9: (f | i) . x = (f | i) . y ; :: thesis: x = y

A10: ( x in dom f & y in dom f ) by A5, A7, A8, XBOOLE_0:def 4;

f . x = (f | i) . x by A4, A7, FUNCT_1:47

.= f . y by A4, A8, A9, FUNCT_1:47 ;

hence x = y by A6, A10; :: thesis: verum

end;let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (f | i) or not y in dom (f | i) or not (f | i) . x = (f | i) . y or x = y )

assume that

A7: x in dom (f | i) and

A8: y in dom (f | i) and

A9: (f | i) . x = (f | i) . y ; :: thesis: x = y

A10: ( x in dom f & y in dom f ) by A5, A7, A8, XBOOLE_0:def 4;

f . x = (f | i) . x by A4, A7, FUNCT_1:47

.= f . y by A4, A8, A9, FUNCT_1:47 ;

hence x = y by A6, A10; :: thesis: verum

A12: i in NAT by ORDINAL1:def 12;

Seg (len f) = dom f by FINSEQ_1:def 3;

then Seg i c= dom f by A11, FINSEQ_1:5;

then A13: dom (f | i) = Seg i by A5, XBOOLE_1:28;

hence len (f | i) >= 2 by A1, A12, FINSEQ_1:def 3; :: thesis: ( f | i is unfolded & f | i is s.n.c. & f | i is special )

A14: f is unfolded by A3;

thus f | i is unfolded :: thesis: ( f | i is s.n.c. & f | i is special )

proof

A21:
f is s.n.c.
by A3;
let j be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= j or not j + 2 <= len (f | i) or (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} )

assume that

A15: 1 <= j and

A16: j + 2 <= len (f | i) ; :: thesis: (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))}

j + 1 <= j + 2 by XREAL_1:6;

then A17: j + 1 <= len (f | i) by A16, XXREAL_0:2;

len (f | i) <= len f by A11, A13, A12, FINSEQ_1:def 3;

then A18: j + 2 <= len f by A16, XXREAL_0:2;

1 <= j + 1 by NAT_1:12;

then A19: j + 1 in dom (f | i) by A17, FINSEQ_3:25;

1 <= (j + 1) + 1 by NAT_1:12;

then (j + 1) + 1 in dom (f | i) by A16, FINSEQ_3:25;

then A20: LSeg (f,(j + 1)) = LSeg ((f | i),(j + 1)) by A19, Th17;

j <= j + 2 by NAT_1:11;

then j <= len (f | i) by A16, XXREAL_0:2;

then j in dom (f | i) by A15, FINSEQ_3:25;

then LSeg (f,j) = LSeg ((f | i),j) by A19, Th17;

then (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {(f /. (j + 1))} by A14, A15, A18, A20;

hence (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} by A19, FINSEQ_4:70; :: thesis: verum

end;assume that

A15: 1 <= j and

A16: j + 2 <= len (f | i) ; :: thesis: (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))}

j + 1 <= j + 2 by XREAL_1:6;

then A17: j + 1 <= len (f | i) by A16, XXREAL_0:2;

len (f | i) <= len f by A11, A13, A12, FINSEQ_1:def 3;

then A18: j + 2 <= len f by A16, XXREAL_0:2;

1 <= j + 1 by NAT_1:12;

then A19: j + 1 in dom (f | i) by A17, FINSEQ_3:25;

1 <= (j + 1) + 1 by NAT_1:12;

then (j + 1) + 1 in dom (f | i) by A16, FINSEQ_3:25;

then A20: LSeg (f,(j + 1)) = LSeg ((f | i),(j + 1)) by A19, Th17;

j <= j + 2 by NAT_1:11;

then j <= len (f | i) by A16, XXREAL_0:2;

then j in dom (f | i) by A15, FINSEQ_3:25;

then LSeg (f,j) = LSeg ((f | i),j) by A19, Th17;

then (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {(f /. (j + 1))} by A14, A15, A18, A20;

hence (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} by A19, FINSEQ_4:70; :: thesis: verum

thus f | i is s.n.c. :: thesis: f | i is special

proof

let j be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= j or not j + 1 <= len (f | i) or ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 )
let n, k be Nat; :: according to TOPREAL1:def 7 :: thesis: ( k <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),k) )

A22: k + 1 >= 1 by NAT_1:11;

A23: n + 1 >= 1 by NAT_1:11;

assume n + 1 < k ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),k)

then LSeg (f,n) misses LSeg (f,k) by A21;

then A24: (LSeg (f,n)) /\ (LSeg (f,k)) = {} ;

A25: k + 1 >= k by NAT_1:11;

A26: n + 1 >= n by NAT_1:11;

end;A22: k + 1 >= 1 by NAT_1:11;

A23: n + 1 >= 1 by NAT_1:11;

assume n + 1 < k ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),k)

then LSeg (f,n) misses LSeg (f,k) by A21;

then A24: (LSeg (f,n)) /\ (LSeg (f,k)) = {} ;

A25: k + 1 >= k by NAT_1:11;

A26: n + 1 >= n by NAT_1:11;

per cases
( n in dom (f | i) or not n in dom (f | i) )
;

end;

suppose A27:
n in dom (f | i)
; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),k)

end;

now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} end;

hence
(LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
; :: according to XBOOLE_0:def 7 :: thesis: verumper cases
( n + 1 in dom (f | i) or not n + 1 in dom (f | i) )
;

end;

suppose
n + 1 in dom (f | i)
; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}

then A28:
LSeg (f,n) = LSeg ((f | i),n)
by A27, Th17;

end;now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} end;

hence
(LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
; :: thesis: verumper cases
( k in dom (f | i) or not k in dom (f | i) )
;

end;

suppose A29:
k in dom (f | i)
; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}

end;

now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}

hence
(LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
; :: thesis: verumend;

suppose
not k in dom (f | i)
; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}

then
( k < 1 or k > len (f | i) )
by FINSEQ_3:25;

then ( k < 1 or k + 1 > len (f | i) ) by A25, XXREAL_0:2;

then LSeg ((f | i),k) = {} by TOPREAL1:def 3;

hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum

end;then ( k < 1 or k + 1 > len (f | i) ) by A25, XXREAL_0:2;

then LSeg ((f | i),k) = {} by TOPREAL1:def 3;

hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum

suppose
not n in dom (f | i)
; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),k)

then
( n < 1 or n > len (f | i) )
by FINSEQ_3:25;

then ( n < 1 or n + 1 > len (f | i) ) by A26, XXREAL_0:2;

then LSeg ((f | i),n) = {} by TOPREAL1:def 3;

hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

end;then ( n < 1 or n + 1 > len (f | i) ) by A26, XXREAL_0:2;

then LSeg ((f | i),n) = {} by TOPREAL1:def 3;

hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

assume that

A30: 1 <= j and

A31: j + 1 <= len (f | i) ; :: thesis: ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 )

len (f | i) <= len f by A11, A13, A12, FINSEQ_1:def 3;

then A32: j + 1 <= len f by A31, XXREAL_0:2;

j <= j + 1 by NAT_1:11;

then j <= len (f | i) by A31, XXREAL_0:2;

then j in dom (f | i) by A30, FINSEQ_3:25;

then A33: (f | i) /. j = f /. j by FINSEQ_4:70;

1 <= j + 1 by NAT_1:12;

then j + 1 in dom (f | i) by A31, FINSEQ_3:25;

then A34: (f | i) /. (j + 1) = f /. (j + 1) by FINSEQ_4:70;

f is special by A3;

hence ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 ) by A30, A32, A33, A34; :: thesis: verum