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