set F = FGPrIso s,t;
now let a,
b be
Element of
(pi_1 [:S,T:],[s,t]);
:: thesis: (FGPrIso s,t) . (a * b) = ((FGPrIso s,t) . a) * ((FGPrIso s,t) . b)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;
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;
consider lab being
Loop of
[s,t] such that A5:
a * b = Class (EqRel [:S,T:],[s,t]),
lab
and A6:
(FGPrIso s,t) . (a * b) = <*(Class (EqRel S,s),(pr1 lab)),(Class (EqRel T,t),(pr2 lab))*>
by Def2;
reconsider A1 =
Class (EqRel S,s),
(pr1 la),
A2 =
Class (EqRel S,s),
(pr1 lb) as
Element of
(pi_1 S,s) by TOPALG_1:48;
reconsider B1 =
Class (EqRel T,t),
(pr2 la),
B2 =
Class (EqRel T,t),
(pr2 lb) as
Element of
(pi_1 T,t) by TOPALG_1:48;
a * b = Class (EqRel [:S,T:],[s,t]),
(la + lb)
by A1, A3, TOPALG_1:62;
then A7:
lab,
la + lb are_homotopic
by A5, TOPALG_1:47;
then A8:
pr1 lab,
pr1 (la + lb) are_homotopic
by Th19;
A9:
pr2 lab,
pr2 (la + lb) are_homotopic
by A7, Th20;
A10:
A1 * A2 =
Class (EqRel S,s),
((pr1 la) + (pr1 lb))
by TOPALG_1:62
.=
Class (EqRel S,s),
(pr1 (la + lb))
by Th23
.=
Class (EqRel S,s),
(pr1 lab)
by A8, TOPALG_1:47
;
B1 * B2 =
Class (EqRel T,t),
((pr2 la) + (pr2 lb))
by TOPALG_1:62
.=
Class (EqRel T,t),
(pr2 (la + lb))
by Th25
.=
Class (EqRel T,t),
(pr2 lab)
by A9, TOPALG_1:47
;
hence
(FGPrIso s,t) . (a * b) = ((FGPrIso s,t) . a) * ((FGPrIso s,t) . b)
by A2, A4, A6, A10, GROUP_7:32;
:: thesis: verum end;
hence
FGPrIso s,t is Homomorphism of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>)
by GROUP_6:def 7; :: thesis: verum