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:48;
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