let S, T be non empty TopSpace; :: thesis: 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))*>
let s be Point of S; :: thesis: 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))*>
let t be Point of T; :: thesis: 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))*>
let x be Point of (pi_1 [:S,T:],[s,t]); :: thesis: 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))*>
let l be Loop of [s,t]; :: thesis: ( x = Class (EqRel [:S,T:],[s,t]),l implies (FGPrIso s,t) . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> )
consider l1 being Loop of [s,t] such that
A1: x = Class (EqRel [:S,T:],[s,t]),l1 and
A2: (FGPrIso s,t) . x = <*(Class (EqRel S,s),(pr1 l1)),(Class (EqRel T,t),(pr2 l1))*> by Def2;
assume x = Class (EqRel [:S,T:],[s,t]),l ; :: thesis: (FGPrIso s,t) . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*>
then A3: l,l1 are_homotopic by A1, TOPALG_1:47;
then A4: pr1 l, pr1 l1 are_homotopic by Th19;
pr2 l, pr2 l1 are_homotopic by A3, Th20;
then Class (EqRel T,t),(pr2 l) = Class (EqRel T,t),(pr2 l1) by TOPALG_1:47;
hence (FGPrIso s,t) . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> by A2, A4, TOPALG_1:47; :: thesis: verum