let n be Element of NAT ; :: thesis: 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); :: thesis: 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
;
:: thesis: 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
;
:: thesis: 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:71;
A3:
rng g = {p1}
by FUNCOP_1:14;
the
carrier of
((TOP-REAL n) | (LSeg p1,p2)) = LSeg p1,
p2
by PRE_TOPC:29;
then reconsider f =
g as
Function of
I[01] ,
((TOP-REAL n) | (LSeg p1,p2)) by A2, A3, FUNCT_2:8;
take
f
;
:: thesis: ( rng f = LSeg p1,p2 & g = f )thus
(
rng f = LSeg p1,
p2 &
g = f )
by A1, A3, RLTOPSP1:71;
:: thesis: verum end;