set F = FGPrIso s,t;
let a, b be Element of (pi_1 [:S,T:],[s,t]); GROUP_6:def 7 (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;
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;
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;
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;
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: 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
;
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
;
hence
(FGPrIso s,t) . (a * b) = ((FGPrIso s,t) . a) * ((FGPrIso s,t) . b)
by A2, A4, A6, A10, GROUP_7:32; verum