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 ;
then lsab,lsa + lsb are_homotopic by ;
then f * lsab,(f * lsa) + (f * lsb) are_homotopic by ;
hence (FundGrIso (f,s)) . (a * b) = Class ((EqRel (T,(f . s))),((f * lsa) + (f * lsb))) by
.= ((FundGrIso (f,s)) . a) * ((FundGrIso (f,s)) . b) by ;
:: thesis: verum