let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q )
assume A1: f is weakly-one-to-one ; :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f implies (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q )
assume that
A2: p in L~ f and
A3: q in L~ f ; :: thesis: (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q
A4: B_Cut (f,q,p) <> {} by Th3;
B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A1, A2, A3, Th17;
hence (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = (Rev (B_Cut (f,q,p))) /. (len (B_Cut (f,q,p))) by FINSEQ_5:def 3
.= (B_Cut (f,q,p)) /. 1 by A4, FINSEQ_5:65
.= q by A1, A2, A3, Th19 ;
:: thesis: verum