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

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