let f be S-Sequence_in_R2; for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) = mid (f,1,(p .. f))
let p be Point of (TOP-REAL 2); ( p in rng f implies R_Cut (f,p) = mid (f,1,(p .. f)) )
assume A1:
p in rng f
; R_Cut (f,p) = mid (f,1,(p .. f))
then consider i being Nat such that
A2:
i in dom f
and
A3:
f . i = p
by FINSEQ_2:10;
reconsider i = i as Nat ;
A4:
i <= len f
by A2, FINSEQ_3:25;
len f >= 2
by TOPREAL1:def 8;
then A5:
rng f c= L~ f
by SPPOL_2:18;
then A6:
1 <= Index (p,f)
by A1, JORDAN3:8;
A7:
Index (p,f) < len f
by A1, A5, JORDAN3:8;
A8:
0 + 1 <= i
by A2, FINSEQ_3:25;
then A9:
i - 1 >= 0
by XREAL_1:19;
per cases
( 1 < i or 1 = i )
by A8, XXREAL_0:1;
suppose A10:
1
< i
;
R_Cut (f,p) = mid (f,1,(p .. f))
1
<= len f
by A8, A4, XXREAL_0:2;
then
1
in dom f
by FINSEQ_3:25;
then
p <> f . 1
by A2, A3, A10, FUNCT_1:def 4;
then A11:
R_Cut (
f,
p)
= (mid (f,1,(Index (p,f)))) ^ <*p*>
by JORDAN3:def 4;
A12:
(Index (p,f)) + 1
= i
by A3, A4, A10, JORDAN3:12;
A13:
len (mid (f,1,(Index (p,f)))) =
((Index (p,f)) -' 1) + 1
by A6, A7, JORDAN4:8
.=
i -' 1
by A1, A5, A12, JORDAN3:8, NAT_D:38
;
A14:
len (mid (f,1,i)) =
(i -' 1) + 1
by A8, A4, JORDAN4:8
.=
i
by A8, XREAL_1:235
;
then A15:
dom (mid (f,1,i)) = Seg i
by FINSEQ_1:def 3;
A16:
now for j being Nat st j in dom (mid (f,1,i)) holds
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . jlet j be
Nat;
( j in dom (mid (f,1,i)) implies (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j )reconsider a =
j as
Nat ;
assume A17:
j in dom (mid (f,1,i))
;
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . jthen A18:
1
<= j
by A15, FINSEQ_1:1;
A19:
j <= i
by A15, A17, FINSEQ_1:1;
now (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . jper cases
( j < i or j = i )
by A19, XXREAL_0:1;
suppose
j < i
;
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . jthen A20:
j <= Index (
p,
f)
by A12, NAT_1:13;
then
j <= i -' 1
by A9, A12, XREAL_0:def 2;
then A21:
j in dom (mid (f,1,(Index (p,f))))
by A13, A18, FINSEQ_3:25;
thus (mid (f,1,i)) . j =
f . a
by A4, A18, A19, FINSEQ_6:123
.=
(mid (f,1,(Index (p,f)))) . a
by A7, A18, A20, FINSEQ_6:123
.=
((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
by A21, FINSEQ_1:def 7
;
verum end; suppose A22:
j = i
;
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . jA23:
(i -' 1) + 1
= i
by A8, XREAL_1:235;
thus (mid (f,1,i)) . j =
f . a
by A4, A18, A19, FINSEQ_6:123
.=
((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
by A3, A13, A22, A23, FINSEQ_1:42
;
verum end; end; end; hence
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
;
verum end; len ((mid (f,1,(Index (p,f)))) ^ <*p*>) =
(i -' 1) + 1
by A13, FINSEQ_2:16
.=
i
by A8, XREAL_1:235
;
then
mid (
f,1,
i)
= R_Cut (
f,
p)
by A11, A14, A16, FINSEQ_2:9;
hence
R_Cut (
f,
p)
= mid (
f,1,
(p .. f))
by A2, A3, FINSEQ_5:11;
verum end; suppose A24:
1
= i
;
R_Cut (f,p) = mid (f,1,(p .. f))then A25:
R_Cut (
f,
p)
= <*p*>
by A3, JORDAN3:def 4;
A26:
p = f /. 1
by A2, A3, A24, PARTFUN1:def 6;
then S:
p .. f = 1
by FINSEQ_6:43;
f /. 1
= f . 1
by A2, PARTFUN1:def 6, A24;
hence
R_Cut (
f,
p)
= mid (
f,1,
(p .. f))
by A2, A24, A25, A26, S, JORDAN4:15;
verum end; end;