:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def 2 :
for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being Function of I[01],T
for b₅ being Function of [:I[01],I[01]:],T holds
( b₅ = ConvexHomotopy (P,Q) iff for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b₅ . (s,t) = ((1 - t) * a1) + (t * b1) );