let T be non empty having_trivial_Fundamental_Group TopSpace; for t being Point of T
for P1, P2 being Loop of t holds P1,P2 are_homotopic
let t be Point of T; for P1, P2 being Loop of t holds P1,P2 are_homotopic
let P1, P2 be Loop of t; 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; verum