set F = FGPrIso s,t;
set G = <*(pi_1 S,s),(pi_1 T,t)*>;
set pS = pi_1 [:S,T:],[s,t];
set pT = product <*(pi_1 S,s),(pi_1 T,t)*>;
A1: 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;
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 proj1 (FGPrIso s,t) or not b in proj1 (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 proj1 (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
A2: a = Class (EqRel [:S,T:],[s,t]),la and
A3: (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
A4: b = Class (EqRel [:S,T:],[s,t]),lb and
A5: (FGPrIso s,t) . b = <*(Class (EqRel S,s),(pr1 lb)),(Class (EqRel T,t),(pr2 lb))*> by Def2;
assume A6: (FGPrIso s,t) . a = (FGPrIso s,t) . b ; :: thesis: a = b
then Class (EqRel T,t),(pr2 la) = Class (EqRel T,t),(pr2 lb) by A3, A5, FINSEQ_1:98;
then A7: pr2 la, pr2 lb are_homotopic by TOPALG_1:47;
Class (EqRel S,s),(pr1 la) = Class (EqRel S,s),(pr1 lb) by A3, A5, A6, FINSEQ_1:98;
then pr1 la, pr1 lb are_homotopic by TOPALG_1:47;
then la,lb are_homotopic by A7, Th22;
hence a = b by A2, A4, 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= proj2 (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 proj2 (FGPrIso s,t) )
assume y in the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) ; :: thesis: y in proj2 (FGPrIso s,t)
then consider g being Function such that
A8: y = g and
A9: dom g = dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) and
A10: 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 A1, CARD_3:def 5;
A11: dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) = {1,2} by PARTFUN1:def 4;
then reconsider g = g as FinSequence by A9, FINSEQ_1:4, FINSEQ_1:def 2;
A12: len g = 2 by A9, A11, FINSEQ_1:4, FINSEQ_1:def 3;
A13: ( 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 ) & <*(pi_1 S,s),(pi_1 T,t)*> . 2 = pi_1 T,t ) by Lm2, FINSEQ_1:61, PRALG_1:def 13;
g . 2 in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 2 by A10, A11, Lm2;
then consider l2 being Loop of t such that
A14: g . 2 = Class (EqRel T,t),l2 by A13, TOPALG_1:48;
A15: ( 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 ) & <*(pi_1 S,s),(pi_1 T,t)*> . 1 = pi_1 S,s ) by Lm1, FINSEQ_1:61, PRALG_1:def 13;
g . 1 in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . 1 by A10, A11, Lm1;
then consider l1 being Loop of s such that
A16: g . 1 = Class (EqRel S,s),l1 by A15, TOPALG_1:48;
set x = Class (EqRel [:S,T:],[s,t]),<:l1,l2:>;
A17: dom l1 = the carrier of I[01] by FUNCT_2:def 1
.= dom l2 by FUNCT_2:def 1 ;
dom (FGPrIso s,t) = the carrier of (pi_1 [:S,T:],[s,t]) by FUNCT_2:def 1;
then A18: Class (EqRel [:S,T:],[s,t]),<:l1,l2:> in dom (FGPrIso s,t) by TOPALG_1:48;
(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 A17, Th7
.= <*(Class (EqRel S,s),l1),(Class (EqRel T,t),l2)*> by A17, Th8
.= y by A8, A12, A16, A14, FINSEQ_1:61 ;
hence y in proj2 (FGPrIso s,t) by A18, FUNCT_1:def 5; :: thesis: verum