:: deftheorem Def4 defines R1Homotopy TOPALG_2:def 4 :
for T being non empty interval SubSpace of R^1
for P, Q being Function of I[01],T
for b₄ being Function of [:I[01],I[01]:],T holds
( b₄ = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b₄ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );