set pS = pi_1 S,s;
set h = FundGrIso f,s;
now let a,
b be
Element of
(pi_1 S,s);
:: thesis: (FundGrIso f,s) . (a * b) = ((FundGrIso f,s) . a) * ((FundGrIso f,s) . b)consider lsa being
Loop of
s such that A1:
a = Class (EqRel S,s),
lsa
and A2:
(FundGrIso f,s) . a = Class (EqRel T,(f . s)),
(f * lsa)
by Def1;
consider lsb being
Loop of
s such that A3:
b = Class (EqRel S,s),
lsb
and A4:
(FundGrIso f,s) . b = Class (EqRel T,(f . s)),
(f * lsb)
by Def1;
consider lsab being
Loop of
s such that A5:
a * b = Class (EqRel S,s),
lsab
and A6:
(FundGrIso f,s) . (a * b) = Class (EqRel T,(f . s)),
(f * lsab)
by Def1;
A7:
(f * lsa) + (f * lsb) = f * (lsa + lsb)
by Th30;
a * b = Class (EqRel S,s),
(lsa + lsb)
by A1, A3, TOPALG_1:62;
then
lsab,
lsa + lsb are_homotopic
by A5, TOPALG_1:47;
then
f * lsab,
(f * lsa) + (f * lsb) are_homotopic
by A7, Th28;
hence (FundGrIso f,s) . (a * b) =
Class (EqRel T,(f . s)),
((f * lsa) + (f * lsb))
by A6, TOPALG_1:47
.=
((FundGrIso f,s) . a) * ((FundGrIso f,s) . b)
by A2, A4, TOPALG_1:62
;
:: thesis: verum end;
hence
FundGrIso f,s is Homomorphism of (pi_1 S,s),(pi_1 T,(f . s))
by GROUP_6:def 7; :: thesis: verum