let n be Nat; :: thesis: ( n >= 2 implies TUnitSphere n is having_trivial_Fundamental_Group )
assume A1: n >= 2 ; :: thesis: TUnitSphere n is having_trivial_Fundamental_Group
set T = TUnitSphere n;
for t being Point of (TUnitSphere n)
for f being Loop of t holds f is nullhomotopic

proof

let t be Point of (TUnitSphere n); :: thesis: for f being Loop of t holds f is nullhomotopic
let f be Loop of t; :: thesis: f is nullhomotopic

per cases ( rng f <> the carrier of (TUnitSphere n) or rng f = the carrier of (TUnitSphere n) ) ;

suppose rng f <> the carrier of (TUnitSphere n) ; :: thesis: f is nullhomotopic

hence f is nullhomotopic by Lm3; :: thesis: verum

end;

suppose rng f = the carrier of (TUnitSphere n) ; :: thesis: f is nullhomotopic

then consider g being Loop of t such that
A2: g,f are_homotopic and
A3: rng g <> the carrier of (TUnitSphere n) by A1, Lm4;
g is nullhomotopic by A3, Lm3;
then consider C being constant Loop of t such that
A4: g,C are_homotopic ;
f,C are_homotopic by A2, A4, BORSUK_6:79;
hence f is nullhomotopic ; :: thesis: verum

end;

end;

end;

hence TUnitSphere n is having_trivial_Fundamental_Group by Th17; :: thesis: verum