let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds
(L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f)
let p be Point of (TOP-REAL 2); ( f is being_S-Seq & p in L~ f implies (L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f) )
assume that
A1:
f is being_S-Seq
and
A2:
p in L~ f
; (L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f)
A3:
len f in dom f
by A1, FINSEQ_5:6;
L_Cut (f,p) <> {}
by A2, JORDAN1E:3;
then
len (L_Cut (f,p)) in dom (L_Cut (f,p))
by FINSEQ_5:6;
hence (L_Cut (f,p)) /. (len (L_Cut (f,p))) =
(L_Cut (f,p)) . (len (L_Cut (f,p)))
by PARTFUN1:def 6
.=
f . (len f)
by A1, A2, JORDAN1B:4
.=
f /. (len f)
by A3, PARTFUN1:def 6
;
verum