let X be non empty TopSpace; for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
let a, b, c be Point of X; ( a,b are_connected & c,b are_connected implies for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic )
assume that
A1:
a,b are_connected
and
A2:
c,b are_connected
; for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
set X = the constant Path of b,b;
let A1, A2 be Path of a,b; for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
let B be Path of c,b; ( A1,A2 are_homotopic implies A1,(A2 + (- B)) + B are_homotopic )
A3:
A1,A1 + the constant Path of b,b are_homotopic
by A1, BORSUK_6:80;
assume A4:
A1,A2 are_homotopic
; A1,(A2 + (- B)) + B are_homotopic
(- B) + B, the constant Path of b,b are_homotopic
by A2, BORSUK_6:86;
then
A2 + ((- B) + B),A1 + the constant Path of b,b are_homotopic
by A1, A4, BORSUK_6:75;
then A5:
A2 + ((- B) + B),A1 are_homotopic
by A3, BORSUK_6:79;
A2 + ((- B) + B),(A2 + (- B)) + B are_homotopic
by A1, A2, BORSUK_6:73;
hence
A1,(A2 + (- B)) + B are_homotopic
by A5, BORSUK_6:79; verum