let T be non empty having_trivial_Fundamental_Group TopSpace; :: thesis: for t being Point of T
for P1, P2 being Loop of t holds P1,P2 are_homotopic
let t be Point of T; :: thesis: for P1, P2 being Loop of t holds P1,P2 are_homotopic
let P1, P2 be Loop of t; :: thesis: P1,P2 are_homotopic
( Class ((EqRel (T,t)),P1) in the carrier of (pi_1 (T,t)) & Class ((EqRel (T,t)),P2) in the carrier of (pi_1 (T,t)) ) by TOPALG_1:47;
then Class ((EqRel (T,t)),P1) = Class ((EqRel (T,t)),P2) by ZFMISC_1:def 10;
hence P1,P2 are_homotopic by TOPALG_1:46; :: thesis: verum