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:46;
then pr2 l, pr2 l1 are_homotopic by Th20;
then A4: Class ((EqRel (T,t)),(pr2 l)) = Class ((EqRel (T,t)),(pr2 l1)) by TOPALG_1:46;
pr1 l, pr1 l1 are_homotopic by A3, Th19;
hence (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> by A2, A4, TOPALG_1:46; :: thesis: verum