let T be non empty pathwise_connected TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b
for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds
RePar (P,f),P are_homotopic
let a, b be Point of T; :: thesis: for P being Path of a,b
for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds
RePar (P,f),P are_homotopic
let P be Path of a,b; :: thesis: for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds
RePar (P,f),P are_homotopic
let f be continuous Function of I[01],I[01]; :: thesis: ( f . 0 = 0 & f . 1 = 1 implies RePar (P,f),P are_homotopic )
a,b are_connected by BORSUK_2:def 3;
hence ( f . 0 = 0 & f . 1 = 1 implies RePar (P,f),P are_homotopic ) by Th53; :: thesis: verum