let T be non empty TopSpace; :: thesis: for a being Point of T ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a )
let a be Point of T; :: thesis: ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a )
take I[01] --> a ; :: thesis: ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a )
thus ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def 14, BORSUK_1:def 15, FUNCOP_1:7; :: thesis: verum