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