let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is weakly-one-to-one & len f >= 2 holds
L_Cut f,(f /. 1) = f
let p be Point of (TOP-REAL 2); :: thesis: ( f is weakly-one-to-one & len f >= 2 implies L_Cut f,(f /. 1) = f )
assume that
A1: f is weakly-one-to-one and
A2: len f >= 2 ; :: thesis: L_Cut f,(f /. 1) = f
A3: Index (f /. 1),f = 1 by A2, JORDAN3:44;
1 <= len f by A2, XXREAL_0:2;
then A4: 1 in dom f by FINSEQ_3:27;
then A5: f /. 1 = f . 1 by PARTFUN1:def 8;
2 = 1 + 1 ;
then A6: 1 < len f by A2, NAT_1:13;
then f . 1 <> f . (1 + 1) by A1, Def2;
then f /. 1 <> f . (1 + 1) by A4, PARTFUN1:def 8;
hence L_Cut f,(f /. 1) = <*(f /. 1)*> ^ (mid f,((Index (f /. 1),f) + 1),(len f)) by A3, JORDAN3:def 4
.= mid f,1,(len f) by A4, A6, A5, A3, FINSEQ_6:132
.= f by A2, FINSEQ_6:126, XXREAL_0:2 ;
:: thesis: verum