let n be Element of NAT ; for p1, p2 being Point of (TOP-REAL n) ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( rng f = LSeg (p1,p2) & F = f )
let p1, p2 be Point of (TOP-REAL n); ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( rng f = LSeg (p1,p2) & F = f )
per cases
( p1 = p2 or p1 <> p2 )
;
suppose A1:
p1 = p2
;
ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( rng f = LSeg (p1,p2) & F = f )then reconsider g =
I[01] --> p1 as
Path of
p1,
p2 by Th41;
take
g
;
ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( rng f = LSeg (p1,p2) & g = f )A2:
LSeg (
p1,
p2)
= {p1}
by A1, RLTOPSP1:70;
A3:
rng g = {p1}
by FUNCOP_1:8;
the
carrier of
((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (
p1,
p2)
by PRE_TOPC:8;
then reconsider f =
g as
Function of
I[01],
((TOP-REAL n) | (LSeg (p1,p2))) by A2, A3, FUNCT_2:6;
take
f
;
( rng f = LSeg (p1,p2) & g = f )thus
(
rng f = LSeg (
p1,
p2) &
g = f )
by A1, A3, RLTOPSP1:70;
verum end;