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:90;
thus
f | i is one-to-one
TOPREAL1:def 10 ( 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 10;
let x be
set ;
FUNCT_1:def 8 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:70
.=
f . y
by A4, A8, A9, FUNCT_1:70
;
hence
x = y
by A6, A10, FUNCT_1:def 8;
verum
end;
A11:
i <= len f
by A2, FINSEQ_3:27;
Seg (len f) = dom f
by FINSEQ_1:def 3;
then
Seg i c= dom f
by A11, FINSEQ_1:7;
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 10;
thus
f | i is unfolded
( f | i is s.n.c. & f | i is special )proof
let j be
Nat;
TOPREAL1:def 8 ( 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:8;
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:27;
1
<= (j + 1) + 1
by NAT_1:12;
then
(j + 1) + 1
in dom (f | i)
by A15, FINSEQ_3:27;
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:27;
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 8;
hence
(LSeg (f | i),j) /\ (LSeg (f | i),(j + 1)) = {((f | i) /. (j + 1))}
by A18, FINSEQ_4:85;
verum
end;
A20:
f is s.n.c.
by A3, TOPREAL1:def 10;
thus
f | i is s.n.c.
f | i is special proof
let n,
k be
Nat;
TOPREAL1:def 9 ( 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 9;
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 7 ( 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:27;
then A32:
(f | i) /. j = f /. j
by FINSEQ_4:85;
1 <= j + 1
by NAT_1:12;
then
j + 1 in dom (f | i)
by A30, FINSEQ_3:27;
then A33:
(f | i) /. (j + 1) = f /. (j + 1)
by FINSEQ_4:85;
f is special
by A3, TOPREAL1:def 10;
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 7; verum