let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ f holds
( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) )
let p be Point of (TOP-REAL 2); ( p in L~ f implies ( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) ) )
assume A1:
p in L~ f
; ( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) )
then A2:
Index (p,f) < len f
by Th8;
now (R_Cut (f,p)) . (len (R_Cut (f,p))) = pper cases
( p <> f . 1 or p = f . 1 )
;
suppose A3:
p <> f . 1
;
(R_Cut (f,p)) . (len (R_Cut (f,p))) = pA4:
len ((mid (f,1,(Index (p,f)))) ^ <*p*>) =
(len (mid (f,1,(Index (p,f))))) + (len <*p*>)
by FINSEQ_1:22
.=
(len (mid (f,1,(Index (p,f))))) + 1
by FINSEQ_1:39
;
R_Cut (
f,
p)
= (mid (f,1,(Index (p,f)))) ^ <*p*>
by A3, Def4;
hence
(R_Cut (f,p)) . (len (R_Cut (f,p))) = p
by A4, FINSEQ_1:42;
verum end; end; end;
hence
(R_Cut (f,p)) . (len (R_Cut (f,p))) = p
; for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i
A6:
1 <= Index (p,f)
by A1, Th8;
then
len f > 1
by A2, XXREAL_0:2;
then A7: len (mid (f,1,(Index (p,f)))) =
((Index (p,f)) -' 1) + 1
by A6, A2, FINSEQ_6:118
.=
Index (p,f)
by A1, Th8, XREAL_1:235
;
thus
for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i
verumproof
let i be
Element of
NAT ;
( 1 <= i & i <= Index (p,f) implies (R_Cut (f,p)) . i = f . i )
assume that A8:
1
<= i
and A9:
i <= Index (
p,
f)
;
(R_Cut (f,p)) . i = f . i
now ( ( p <> f . 1 & (R_Cut (f,p)) . i = f . i ) or ( p = f . 1 & (R_Cut (f,p)) . i = f . i ) )per cases
( p <> f . 1 or p = f . 1 )
;
case
p <> f . 1
;
(R_Cut (f,p)) . i = f . ithen (R_Cut (f,p)) . i =
((mid (f,1,(Index (p,f)))) ^ <*p*>) . i
by Def4
.=
(mid (f,1,(Index (p,f)))) . i
by A7, A8, A9, FINSEQ_1:64
.=
f . i
by A2, A8, A9, FINSEQ_6:123
;
hence
(R_Cut (f,p)) . i = f . i
;
verum end; case A10:
p = f . 1
;
(R_Cut (f,p)) . i = f . iA11:
len f > 1
by A6, A2, XXREAL_0:2;
then
1
in dom f
by FINSEQ_3:25;
then A12:
p = f /. 1
by A10, PARTFUN1:def 6;
len f >= 1
+ 1
by A11, NAT_1:13;
then
Index (
p,
f)
= 1
by A12, Th11;
then A13:
i = 1
by A8, A9, XXREAL_0:1;
R_Cut (
f,
p)
= <*p*>
by A10, Def4;
hence
(R_Cut (f,p)) . i = f . i
by A10, A13, FINSEQ_1:40;
verum end; end; end;
hence
(R_Cut (f,p)) . i = f . i
;
verum
end;