theorem Th28: :: TOPALG_4:28

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*>