let S be non empty TopSpace; :: thesis: 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))
let s be Point of S; :: thesis: 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))
set X = pi_1 (S,s);
let x, y be Element of (pi_1 (S,s)); :: thesis: 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))
let P, Q be Loop of s; :: thesis: ( x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) implies x * y = Class ((EqRel (S,s)),(P + Q)) )
consider P1, Q1 being Loop of s such that
A1: ( x = Class ((EqRel (S,s)),P1) & y = Class ((EqRel (S,s)),Q1) ) and
A2: the multF of (pi_1 (S,s)) . (x,y) = Class ((EqRel (S,s)),(P1 + Q1)) by Def5;
assume ( x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) ) ; :: thesis: x * y = Class ((EqRel (S,s)),(P + Q))
then ( P,P1 are_homotopic & Q,Q1 are_homotopic ) by A1, Th46;
then P + Q,P1 + Q1 are_homotopic by BORSUK_6:75;
hence x * y = Class ((EqRel (S,s)),(P + Q)) by A2, Th46; :: thesis: verum