let S, T be non empty TopSpace; :: thesis: 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)))*>
let s be Point of S; :: thesis: 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)))*>
let t be Point of T; :: thesis: 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)))*>
let l be Loop of [s,t]; :: thesis: (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*>
Class ((EqRel ([:S,T:],[s,t])),l) is Point of (pi_1 ([:S,T:],[s,t])) by TOPALG_1:47;
hence (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> by Th27; :: thesis: verum