:: deftheorem Def7 defines RealHomotopy TOPALG_1:def 7 :
for n being Nat
for P, Q being Function of I[01],(TOP-REAL n)
for b₄ being Function of [:I[01],I[01]:],(TOP-REAL n) holds
( b₄ = RealHomotopy (P,Q) iff for s, t being Element of I[01] holds b₄ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );