for T being non empty TopSpace
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 & a,b are_connected holds
RePar (P,f),P are_homotopic