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
FGPrIso (s,t) is onto proof
let a,
b be
object ;
FUNCT_1:def 4 ( 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))
;
( 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))
;
( 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
;
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;
verum
end;
thus
rng (FGPrIso (s,t)) c= the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>)
; XBOOLE_0:def 10,FUNCT_2:def 3 the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) c= rng (FGPrIso (s,t))
let y be object ; TARSKI:def 3 ( 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))*>)
; 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, FINSEQ_1:44, 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, FINSEQ_1:44, 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; verum