let X be non empty TopSpace; :: thesis: for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
let a, b, c, d, e be Point of X; :: thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected implies for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic )
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: c,d are_connected and
A4: d,e are_connected ; :: thesis: for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
let A be Path of a,b; :: thesis: for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
let B be Path of b,c; :: thesis: for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
let C be Path of c,d; :: thesis: for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
let D be Path of d,e; :: thesis: ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
A5: (A + B) + C,A + (B + C) are_homotopic by A1, A2, A3, BORSUK_6:81;
a,c are_connected by A1, A2, BORSUK_6:46;
then A6: a,d are_connected by A3, BORSUK_6:46;
D,D are_homotopic by A4, BORSUK_2:15;
hence ((A + B) + C) + D,(A + (B + C)) + D are_homotopic by A4, A5, A6, BORSUK_6:83; :: thesis: verum