:: deftheorem Def2 defines FGPrIso TOPALG_4:def 2 :
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for b₅ being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds
( b₅ = FGPrIso (s,t) iff for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) & b₅ . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) );