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 )
proof
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;
A11: i <= len f by A2, FINSEQ_3:25;
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
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;
A21: f is s.n.c. by A3;
thus f | i is s.n.c. :: thesis: f | i is special
proof
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;
per cases ( n in dom (f | i) or not n in dom (f | i) ) ;
suppose A27: n in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),k)
now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
per cases ( n + 1 in dom (f | i) or not n + 1 in dom (f | i) ) ;
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;
now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
per cases ( k in dom (f | i) or not k in dom (f | i) ) ;
suppose A29: k in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
per cases ( k + 1 in dom (f | i) or not k + 1 in dom (f | i) ) ;
suppose k + 1 in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} by A24, A28, A29, Th17; :: thesis: verum
end;
suppose not k + 1 in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
then k + 1 > len (f | i) by A22, FINSEQ_3:25;
then LSeg ((f | i),k) = {} by TOPREAL1:def 3;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum
end;
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;
end;
end;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum
end;
suppose not n + 1 in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {}
then n + 1 > len (f | i) by A23, FINSEQ_3:25;
then LSeg ((f | i),n) = {} by TOPREAL1:def 3;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
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;
end;
end;
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 )
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