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

( 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