set c = the constant Loop of t;

set E = EqRel (T,t);

let x, y be Element of (pi_1 (T,t)); :: according to GROUP_1:def 12 :: thesis: x * y = y * x

consider f being Loop of t such that

A1: x = Class ((EqRel (T,t)),f) by TOPALG_1:47;

consider g being Loop of t such that

A2: y = Class ((EqRel (T,t)),g) by TOPALG_1:47;

A3: ( x * y = Class ((EqRel (T,t)),(f + g)) & y * x = Class ((EqRel (T,t)),(g + f)) ) by A1, A2, TOPALG_1:61;

A4: ( f + g = LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)) & g + f = LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) ) by Th11;

A5: LoopMlt (f,g), LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)) are_homotopic by Th12;

A6: LoopMlt (g,f), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by Th12;

LoopMlt (f,g), LoopMlt (g,f) are_homotopic by Th13;

then LoopMlt (f,g), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by A6, BORSUK_6:79;

then LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by A5, BORSUK_6:79;

hence x * y = y * x by A3, A4, TOPALG_1:46; :: thesis: verum

set E = EqRel (T,t);

let x, y be Element of (pi_1 (T,t)); :: according to GROUP_1:def 12 :: thesis: x * y = y * x

consider f being Loop of t such that

A1: x = Class ((EqRel (T,t)),f) by TOPALG_1:47;

consider g being Loop of t such that

A2: y = Class ((EqRel (T,t)),g) by TOPALG_1:47;

A3: ( x * y = Class ((EqRel (T,t)),(f + g)) & y * x = Class ((EqRel (T,t)),(g + f)) ) by A1, A2, TOPALG_1:61;

A4: ( f + g = LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)) & g + f = LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) ) by Th11;

A5: LoopMlt (f,g), LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)) are_homotopic by Th12;

A6: LoopMlt (g,f), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by Th12;

LoopMlt (f,g), LoopMlt (g,f) are_homotopic by Th13;

then LoopMlt (f,g), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by A6, BORSUK_6:79;

then LoopMlt ((f + the constant Loop of t),( the constant Loop of t + g)), LoopMlt ((g + the constant Loop of t),( the constant Loop of t + f)) are_homotopic by A5, BORSUK_6:79;

hence x * y = y * x by A3, A4, TOPALG_1:46; :: thesis: verum