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