let T be non empty TopSpace; :: thesis: ( T is having_trivial_Fundamental_Group implies for t being Point of T
for P, Q being Loop of t holds P,Q are_homotopic )
assume A1: T is having_trivial_Fundamental_Group ; :: thesis: for t being Point of T
for P, Q being Loop of t holds P,Q are_homotopic
let t be Point of T; :: thesis: for P, Q being Loop of t holds P,Q are_homotopic
let P, Q be Loop of t; :: thesis: P,Q are_homotopic
set E = EqRel (T,t);
A2: pi_1 (T,t) is trivial by A1, Def1;
( Class ((EqRel (T,t)),P) in the carrier of (pi_1 (T,t)) & Class ((EqRel (T,t)),Q) in the carrier of (pi_1 (T,t)) ) by TOPALG_1:47;
then Class ((EqRel (T,t)),P) = Class ((EqRel (T,t)),Q) by A2, ZFMISC_1:def 10;
hence P,Q are_homotopic by TOPALG_1:46; :: thesis: verum