Tunit_circle 3 is having_trivial_Fundamental_Group by TOPALG_6:47;
hence for b₁ being Loop of c[100] st b₁ = eLoop i holds
b₁ is nullhomotopic ; :: thesis: verum