:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :
for S, T being non empty TopSpace
for s being Point of S
for f being Function of S,T st f is continuous holds
for b₅ being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) holds
( b₅ = FundGrIso (f,s) iff for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₅ . x = Class ((EqRel (T,(f . s))),(f * ls)) ) );