let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: (L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len f)

Rev f is being_S-Seq by A1;

then A3: 2 <= len (Rev f) by TOPREAL1:def 8;

A4: p in L~ (Rev f) by A2, SPPOL_2:22;

then L_Cut ((Rev (Rev f)),p) = Rev (R_Cut ((Rev f),p)) by A1, JORDAN3:22;

hence (L_Cut (f,p)) . (len (L_Cut (f,p))) = (Rev (R_Cut ((Rev f),p))) . (len (R_Cut ((Rev f),p))) by FINSEQ_5:def 3

.= (R_Cut ((Rev f),p)) . 1 by FINSEQ_5:62

.= (Rev f) . 1 by A4, A3, Th3, XXREAL_0:2

.= f . (len f) by FINSEQ_5:62 ;

:: thesis: verum

(L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len f)

let p be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: (L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len f)

Rev f is being_S-Seq by A1;

then A3: 2 <= len (Rev f) by TOPREAL1:def 8;

A4: p in L~ (Rev f) by A2, SPPOL_2:22;

then L_Cut ((Rev (Rev f)),p) = Rev (R_Cut ((Rev f),p)) by A1, JORDAN3:22;

hence (L_Cut (f,p)) . (len (L_Cut (f,p))) = (Rev (R_Cut ((Rev f),p))) . (len (R_Cut ((Rev f),p))) by FINSEQ_5:def 3

.= (R_Cut ((Rev f),p)) . 1 by FINSEQ_5:62

.= (Rev f) . 1 by A4, A3, Th3, XXREAL_0:2

.= f . (len f) by FINSEQ_5:62 ;

:: thesis: verum