let l be Loop of t; :: thesis: l is nullhomotopic
reconsider c = I[01] --> t as constant Loop of t by JORDAN:41;
take c ; :: according to TOPALG_6:def 3 :: thesis: l,c are_homotopic
thus l,c are_homotopic by Th15; :: thesis: verum