let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: ( f is without_antipodals & f is continuous implies H₁(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a )
assume ( f is without_antipodals & f is continuous ) ; :: thesis: H₁(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a
then reconsider g = Sn1->Sn f as continuous Function of (Tunit_circle 3),(Tunit_circle 2) by Lm13;
H₁(f) = g * (eLoop 1) ;
hence H₁(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a ; :: thesis: verum