for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 (S,s))
for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds
x * y = Class ((EqRel (S,s)),(P + Q)) by Lm4;