:: deftheorem Def6 defines pi_1-iso TOPALG_1:def 6 :
for T being non empty TopSpace
for x0, x1 being Point of T
for P being Path of x0,x1 st x0,x1 are_connected holds
for b₅ being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) holds
( b₅ = pi_1-iso P iff for Q being Loop of x1 holds b₅ . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) );