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 object ; :: according to FUNCT_1:def 4 :: 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:77;
then A7: pr2 la, pr2 lb are_homotopic by TOPALG_1:46;
Class ((EqRel (S,s)),(pr1 la)) = Class ((EqRel (S,s)),(pr1 lb)) by A3, A5, A6, FINSEQ_1:77;
then pr1 la, pr1 lb are_homotopic by TOPALG_1:46;
then la,lb are_homotopic by A7, Th22;
hence a = b by A2, A4, TOPALG_1:46; :: 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 object ; :: 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 y in the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) ; :: thesis: y in rng (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 object 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 2;
then reconsider g = g as FinSequence by A9, FINSEQ_1:2, FINSEQ_1:def 2;
A12: len g = 2 by A9, A11, FINSEQ_1:2, 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, PRALG_1:def 15;
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:47;
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, PRALG_1:def 15;
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:47;
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:47;
(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:44 ;
hence y in rng (FGPrIso (s,t)) by A18, FUNCT_1:def 3; :: thesis: verum