let f be FinSequence of (TOP-REAL 2); for i being Element of NAT st i > 2 & i in dom f & f is being_S-Seq holds
f | i is being_S-Seq
let i be Element of NAT ; ( 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
; 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
TOPREAL1:def 8 ( 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, TOPREAL1:def 8;
let x be
set ;
FUNCT_1:def 4 for b1 being set holds
( not x in proj1 (f | i) or not b1 in proj1 (f | i) or not (f | i) . x = (f | i) . b1 or x = b1 )let y be
set ;
( not x in proj1 (f | i) or not y in proj1 (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
;
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, FUNCT_1:def 4;
verum
end;
A11:
i <= len f
by A2, FINSEQ_3:25;
Seg (len f) = dom f
by FINSEQ_1:def 3;
then
Seg i c= dom f
by A11, FINSEQ_1:5;
then A12:
dom (f | i) = Seg i
by A5, XBOOLE_1:28;
hence
len (f | i) >= 2
by A1, FINSEQ_1:def 3; ( f | i is unfolded & f | i is s.n.c. & f | i is special )
A13:
f is unfolded
by A3, TOPREAL1:def 8;
thus
f | i is unfolded
( f | i is s.n.c. & f | i is special )proof
let j be
Nat;
TOPREAL1:def 6 ( 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 A14:
1
<= j
and A15:
j + 2
<= len (f | i)
;
(LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))}
j + 1
<= j + 2
by XREAL_1:6;
then A16:
j + 1
<= len (f | i)
by A15, XXREAL_0:2;
len (f | i) <= len f
by A11, A12, FINSEQ_1:def 3;
then A17:
j + 2
<= len f
by A15, XXREAL_0:2;
1
<= j + 1
by NAT_1:12;
then A18:
j + 1
in dom (f | i)
by A16, FINSEQ_3:25;
1
<= (j + 1) + 1
by NAT_1:12;
then
(j + 1) + 1
in dom (f | i)
by A15, FINSEQ_3:25;
then A19:
LSeg (
f,
(j + 1))
= LSeg (
(f | i),
(j + 1))
by A18, Th24;
j <= j + 2
by NAT_1:11;
then
j <= len (f | i)
by A15, XXREAL_0:2;
then
j in dom (f | i)
by A14, FINSEQ_3:25;
then
LSeg (
f,
j)
= LSeg (
(f | i),
j)
by A18, Th24;
then
(LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {(f /. (j + 1))}
by A13, A14, A17, A19, TOPREAL1:def 6;
hence
(LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))}
by A18, FINSEQ_4:70;
verum
end;
A20:
f is s.n.c.
by A3, TOPREAL1:def 8;
thus
f | i is s.n.c.
f | i is special proof
let n,
k be
Nat;
TOPREAL1:def 7 ( k <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),k) )
A21:
k + 1
>= 1
by NAT_1:11;
A22:
n + 1
>= 1
by NAT_1:11;
assume
n + 1
< k
;
LSeg ((f | i),n) misses LSeg ((f | i),k)
then
LSeg (
f,
n)
misses LSeg (
f,
k)
by A20, TOPREAL1:def 7;
then A23:
(LSeg (f,n)) /\ (LSeg (f,k)) = {}
by XBOOLE_0:def 7;
A24:
k + 1
>= k
by NAT_1:11;
A25:
n + 1
>= n
by NAT_1:11;
end;
let j be Nat; TOPREAL1:def 5 ( 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
A29:
1 <= j
and
A30:
j + 1 <= len (f | i)
; ( ((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, A12, FINSEQ_1:def 3;
then A31:
j + 1 <= len f
by A30, XXREAL_0:2;
j <= j + 1
by NAT_1:11;
then
j <= len (f | i)
by A30, XXREAL_0:2;
then
j in dom (f | i)
by A29, FINSEQ_3:25;
then A32:
(f | i) /. j = f /. j
by FINSEQ_4:70;
1 <= j + 1
by NAT_1:12;
then
j + 1 in dom (f | i)
by A30, FINSEQ_3:25;
then A33:
(f | i) /. (j + 1) = f /. (j + 1)
by FINSEQ_4:70;
f is special
by A3, TOPREAL1:def 8;
hence
( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 )
by A29, A31, A32, A33, TOPREAL1:def 5; verum