let f be non empty FinSequence of (TOP-REAL 2); 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); ( 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
; L_Cut (f,(f /. 1)) = f
A3:
Index ((f /. 1),f) = 1
by A2, JORDAN3:11;
1 <= len f
by A2, XXREAL_0:2;
then A4:
1 in dom f
by FINSEQ_3:25;
then A5:
f /. 1 = f . 1
by PARTFUN1:def 6;
2 = 1 + 1
;
then A6:
1 < len f
by A2, NAT_1:13;
then
f . 1 <> f . (1 + 1)
by A1;
then
f /. 1 <> f . (1 + 1)
by A4, PARTFUN1:def 6;
hence L_Cut (f,(f /. 1)) =
<*(f /. 1)*> ^ (mid (f,((Index ((f /. 1),f)) + 1),(len f)))
by A3, JORDAN3:def 3
.=
mid (f,1,(len f))
by A4, A6, A5, A3, FINSEQ_6:126
.=
f
by A2, FINSEQ_6:120, XXREAL_0:2
;
verum