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;

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

per cases ( p <> f . 1 or p = f . 1 ) ;

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;

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

then R_Cut (f,p) = <*p*> by JORDAN3:def 4;
hence (R_Cut (f,p)) . 1 = f . 1 by A7; :: thesis: verum

end;

end;

end;

hence (R_Cut (f,p)) . 1 = f . 1 ; :: thesis: verum