set pS = pi_1 [:S,T:],[s,t];
set G = <*(pi_1 S,s),(pi_1 T,t)*>;
set pT = product <*(pi_1 S,s),(pi_1 T,t)*>;
set F = FGPrIso s,t;
thus FGPrIso s,t is one-to-one :: thesis: FGPrIso s,t is onto

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in dom (FGPrIso s,t) or not b in dom (FGPrIso s,t) or not (FGPrIso s,t) . a = (FGPrIso s,t) . b or a = b )
assume a in dom (FGPrIso s,t) ; :: thesis: ( not b in dom (FGPrIso s,t) or not (FGPrIso s,t) . a = (FGPrIso s,t) . b or a = b )
then consider la being Loop of [s,t] such that
A1: a = Class (EqRel [:S,T:],[s,t]),la and
A2: (FGPrIso s,t) . a = <*(Class (EqRel S,s),(pr1 la)),(Class (EqRel T,t),(pr2 la))*> by Def2;
assume b in dom (FGPrIso s,t) ; :: thesis: ( not (FGPrIso s,t) . a = (FGPrIso s,t) . b or a = b )
then consider lb being Loop of [s,t] such that
A3: b = Class (EqRel [:S,T:],[s,t]),lb and
A4: (FGPrIso s,t) . b = <*(Class (EqRel S,s),(pr1 lb)),(Class (EqRel T,t),(pr2 lb))*> by Def2;
assume (FGPrIso s,t) . a = (FGPrIso s,t) . b ; :: thesis: a = b
then ( Class (EqRel S,s),(pr1 la) = Class (EqRel S,s),(pr1 lb) & Class (EqRel T,t),(pr2 la) = Class (EqRel T,t),(pr2 lb) ) by A2, A4, GROUP_7:2;
then ( pr1 la, pr1 lb are_homotopic & pr2 la, pr2 lb are_homotopic ) by TOPALG_1:47;
then la,lb are_homotopic by Th22;
hence a = b by A1, A3, TOPALG_1:47; :: thesis: verum

end;

thus rng (FGPrIso s,t) c= the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) c= rng (FGPrIso s,t)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) or y in rng (FGPrIso s,t) )
assume A5: y in the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) ; :: thesis: y in rng (FGPrIso s,t)
the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) = product (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) by GROUP_7:def 2;
then consider g being Function such that
A6: y = g and
A7: dom g = dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) and
A8: for z being set st z in dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) holds
g . z in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . z by A5, CARD_3:def 5;
A9: dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) = {1,2} by PARTFUN1:def 4;
then reconsider g = g as FinSequence by A7, FINSEQ_1:4, FINSEQ_1:def 2;
A10: len g = 2 by A7, A9, FINSEQ_1:4, FINSEQ_1:def 3;
A11: ex R1 being 1-sorted st
( R1 = <*(pi_1 S,s),(pi_1 T,t)*> . 1 & (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 1 = the carrier of R1 ) by Lm1, PRALG_1:def 13;
A12: ex R2 being 1-sorted st
( R2 = <*(pi_1 S,s),(pi_1 T,t)*> . 2 & (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 2 = the carrier of R2 ) by Lm2, PRALG_1:def 13;
A13: <*(pi_1 S,s),(pi_1 T,t)*> . 1 = pi_1 S,s by FINSEQ_1:61;
A14: <*(pi_1 S,s),(pi_1 T,t)*> . 2 = pi_1 T,t by FINSEQ_1:61;
g . 1 in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 1 by A8, A9, Lm1;
then consider l1 being Loop of s such that
A15: g . 1 = Class (EqRel S,s),l1 by A11, A13, TOPALG_1:48;
g . 2 in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 2 by A8, A9, Lm2;
then consider l2 being Loop of t such that
A16: g . 2 = Class (EqRel T,t),l2 by A12, A14, TOPALG_1:48;
set x = Class (EqRel [:S,T:],[s,t]),<:l1,l2:>;
dom (FGPrIso s,t) = the carrier of (pi_1 [:S,T:],[s,t]) by FUNCT_2:def 1;
then A17: Class (EqRel [:S,T:],[s,t]),<:l1,l2:> in dom (FGPrIso s,t) by TOPALG_1:48;
A18: dom l1 = the carrier of I[01] by FUNCT_2:def 1
.= dom l2 by FUNCT_2:def 1 ;
(FGPrIso s,t) . (Class (EqRel [:S,T:],[s,t]),<:l1,l2:>) = <*(Class (EqRel S,s),(pr1 <:l1,l2:>)),(Class (EqRel T,t),(pr2 <:l1,l2:>))*> by Th28
.= <*(Class (EqRel S,s),l1),(Class (EqRel T,t),(pr2 <:l1,l2:>))*> by A18, Th7
.= <*(Class (EqRel S,s),l1),(Class (EqRel T,t),l2)*> by A18, Th8
.= y by A6, A10, A15, A16, FINSEQ_1:61 ;
hence y in rng (FGPrIso s,t) by A17, FUNCT_1:def 5; :: thesis: verum