let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let S be non empty SubSpace of T; :: thesis: for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let t1, t2 be Point of T; :: thesis: for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let s1, s2 be Point of S; :: thesis: for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let A, B be Path of t1,t2; :: thesis: for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let C, D be Path of s1,s2; :: thesis: ( s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic implies A,B are_homotopic )

assume that

A1: ( s1,s2 are_connected & t1,t2 are_connected ) and

A2: ( A = C & B = D ) ; :: thesis: ( not C,D are_homotopic or A,B are_homotopic )

given f being Function of [:I[01],I[01]:],S such that A3: f is continuous and

A4: for t being Point of I[01] holds

( f . (t,0) = C . t & f . (t,1) = D . t & f . (0,t) = s1 & f . (1,t) = s2 ) ; :: according to BORSUK_2:def 7 :: thesis: A,B are_homotopic

reconsider g = f as Function of [:I[01],I[01]:],T by TOPREALA:7;

take g ; :: according to BORSUK_2:def 7 :: thesis: ( g is continuous & ( for b_{1} being Element of the carrier of I[01] holds

( g . (b_{1},0) = A . b_{1} & g . (b_{1},1) = B . b_{1} & g . (0,b_{1}) = t1 & g . (1,b_{1}) = t2 ) ) )

thus g is continuous by A3, PRE_TOPC:26; :: thesis: for b_{1} being Element of the carrier of I[01] holds

( g . (b_{1},0) = A . b_{1} & g . (b_{1},1) = B . b_{1} & g . (0,b_{1}) = t1 & g . (1,b_{1}) = t2 )

( s1 = C . 0 & s2 = C . 1 & t1 = A . 0 & t2 = A . 1 ) by A1, BORSUK_2:def 2;

hence for b_{1} being Element of the carrier of I[01] holds

( g . (b_{1},0) = A . b_{1} & g . (b_{1},1) = B . b_{1} & g . (0,b_{1}) = t1 & g . (1,b_{1}) = t2 )
by A2, A4; :: thesis: verum

for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let S be non empty SubSpace of T; :: thesis: for t1, t2 being Point of T

for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let t1, t2 be Point of T; :: thesis: for s1, s2 being Point of S

for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let s1, s2 be Point of S; :: thesis: for A, B being Path of t1,t2

for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let A, B be Path of t1,t2; :: thesis: for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds

A,B are_homotopic

let C, D be Path of s1,s2; :: thesis: ( s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic implies A,B are_homotopic )

assume that

A1: ( s1,s2 are_connected & t1,t2 are_connected ) and

A2: ( A = C & B = D ) ; :: thesis: ( not C,D are_homotopic or A,B are_homotopic )

given f being Function of [:I[01],I[01]:],S such that A3: f is continuous and

A4: for t being Point of I[01] holds

( f . (t,0) = C . t & f . (t,1) = D . t & f . (0,t) = s1 & f . (1,t) = s2 ) ; :: according to BORSUK_2:def 7 :: thesis: A,B are_homotopic

reconsider g = f as Function of [:I[01],I[01]:],T by TOPREALA:7;

take g ; :: according to BORSUK_2:def 7 :: thesis: ( g is continuous & ( for b

( g . (b

thus g is continuous by A3, PRE_TOPC:26; :: thesis: for b

( g . (b

( s1 = C . 0 & s2 = C . 1 & t1 = A . 0 & t2 = A . 1 ) by A1, BORSUK_2:def 2;

hence for b

( g . (b