set h = FundGrIso (f,s);
set pS = pi_1 (S,s);
let a, b be Element of (pi_1 (S,s)); :: according to GROUP_6:def 6 :: 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;
A5: (f * lsa) + (f * lsb) = f * (lsa + lsb) by Th29;
consider lsab being Loop of s such that
A6: a * b = Class ((EqRel (S,s)),lsab) and
A7: (FundGrIso (f,s)) . (a * b) = Class ((EqRel (T,(f . s))),(f * lsab)) by Def1;
a * b = Class ((EqRel (S,s)),(lsa + lsb)) by A1, A3, TOPALG_1:61;
then lsab,lsa + lsb are_homotopic by A6, TOPALG_1:46;
then f * lsab,(f * lsa) + (f * lsb) are_homotopic by A5, Th27;
hence (FundGrIso (f,s)) . (a * b) = Class ((EqRel (T,(f . s))),((f * lsa) + (f * lsb))) by A7, TOPALG_1:46
.= ((FundGrIso (f,s)) . a) * ((FundGrIso (f,s)) . b) by A2, A4, TOPALG_1:61 ;
:: thesis: verum