theorem :: TOPALG_3:30

for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))