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 7 :: 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 Th30;
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:62;
then lsab,lsa + lsb are_homotopic by A6, TOPALG_1:47;
then f * lsab,(f * lsa) + (f * lsb) are_homotopic by A5, Th28;
hence (FundGrIso f,s) . (a * b) = Class (EqRel T,(f . s)),((f * lsa) + (f * lsb)) by A7, TOPALG_1:47
.= ((FundGrIso f,s) . a) * ((FundGrIso f,s) . b) by A2, A4, TOPALG_1:62 ;
:: thesis: verum