let X be non empty TopSpace; :: thesis: for a, b, c, d, e, f being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f 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
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
let a, b, c, d, e, f be Point of X; :: thesis: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f 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
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic )
assume that
A1: ( a,b are_connected & b,c are_connected ) and
A2: ( c,d are_connected & d,e are_connected ) and
A3: a,f 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
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + 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
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + 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
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
let C be Path of c,d; :: thesis: for D being Path of d,e
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
let D be Path of d,e; :: thesis: for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
let E be Path of f,c; :: thesis: (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
A4: (A + B) + (- E),(A + B) + (- E) are_homotopic by A3, BORSUK_2:12;
A5: a,c are_connected by A1, BORSUK_6:42;
then A6: f,c are_connected by A3, BORSUK_6:42;
then A7: E + (C + D),(E + C) + D are_homotopic by A2, BORSUK_6:73;
A8: c,e are_connected by A2, BORSUK_6:42;
then A9: ((A + B) + (- E)) + (E + (C + D)),(((A + B) + (- E)) + E) + (C + D) are_homotopic by A3, A6, BORSUK_6:73;
A10: (A + B) + (C + D),(A + (B + C)) + D are_homotopic by A1, A2, Th35;
f,e are_connected by A8, A6, BORSUK_6:42;
then ((A + B) + (- E)) + (E + (C + D)),((A + B) + (- E)) + ((E + C) + D) are_homotopic by A3, A7, A4, BORSUK_6:75;
then A11: (((A + B) + (- E)) + E) + (C + D),((A + B) + (- E)) + ((E + C) + D) are_homotopic by A9, BORSUK_6:79;
(((A + B) + (- E)) + E) + (C + D),(A + B) + (C + D) are_homotopic by A5, A8, A6, Th37;
then (A + (B + C)) + D,(((A + B) + (- E)) + E) + (C + D) are_homotopic by A10, BORSUK_6:79;
hence (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic by A11, BORSUK_6:79; :: thesis: verum