let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st 1 <= len f & p in L~ f holds

(R_Cut (f,p)) . 1 = f . 1

let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= len f & p in L~ f implies (R_Cut (f,p)) . 1 = f . 1 )

assume that

A1: 1 <= len f and

A2: p in L~ f ; :: thesis: (R_Cut (f,p)) . 1 = f . 1

A3: 1 <= Index (p,f) by A2, JORDAN3:8;

A4: 1 in dom f by A1, FINSEQ_3:25;

(R_Cut (f,p)) . 1 = f . 1

let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= len f & p in L~ f implies (R_Cut (f,p)) . 1 = f . 1 )

assume that

A1: 1 <= len f and

A2: p in L~ f ; :: thesis: (R_Cut (f,p)) . 1 = f . 1

A3: 1 <= Index (p,f) by A2, JORDAN3:8;

A4: 1 in dom f by A1, FINSEQ_3:25;

now :: thesis: (R_Cut (f,p)) . 1 = f . 1end;

hence
(R_Cut (f,p)) . 1 = f . 1
; :: thesis: verumper cases
( p <> f . 1 or p = f . 1 )
;

end;

suppose
p <> f . 1
; :: thesis: (R_Cut (f,p)) . 1 = f . 1

then A5:
R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*>
by JORDAN3:def 4;

A6: Index (p,f) < len f by A2, JORDAN3:8;

then Index (p,f) in dom f by A3, FINSEQ_3:25;

then len (mid (f,1,(Index (p,f)))) >= 1 by A4, SPRECT_2:5;

hence (R_Cut (f,p)) . 1 = (mid (f,1,(Index (p,f)))) . 1 by A5, FINSEQ_6:109

.= f . 1 by A1, A3, A6, FINSEQ_6:118 ;

:: thesis: verum

end;A6: Index (p,f) < len f by A2, JORDAN3:8;

then Index (p,f) in dom f by A3, FINSEQ_3:25;

then len (mid (f,1,(Index (p,f)))) >= 1 by A4, SPRECT_2:5;

hence (R_Cut (f,p)) . 1 = (mid (f,1,(Index (p,f)))) . 1 by A5, FINSEQ_6:109

.= f . 1 by A1, A3, A6, FINSEQ_6:118 ;

:: thesis: verum