theorem :: TOPALG_5:18

for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b
for H being Homotopy of P,Q
for t being Point of I[01] st H is continuous holds
Prj1 (t,H) is continuous ;