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:41;
A4: 1 in dom f by A1, FINSEQ_3:27;

now

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 5;
A6: Index p,f < len f by A2, JORDAN3:41;
then Index p,f in dom f by A3, FINSEQ_3:27;
then len (mid f,1,(Index p,f)) >= 1 by A4, SPRECT_2:9;
hence (R_Cut f,p) . 1 = (mid f,1,(Index p,f)) . 1 by A5, JORDAN3:17
.= f . 1 by A1, A3, A6, JORDAN3:27 ;
:: 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 5;
hence (R_Cut f,p) . 1 = f . 1 by A7, FINSEQ_1:57; :: thesis: verum

end;

end;

end;

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