let T be non empty arcwise_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