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, Th47;
then P + Q,P1 + Q1 are_homotopic by BORSUK_6:83;
hence x * y = Class (EqRel S,s),(P + Q) by A2, Th47; :: thesis: verum