for T, U being non empty TopSpace
for t being Point of T
for f being Loop of t
for g being continuous Function of T,U st f is nullhomotopic holds
g * f is nullhomotopic