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₁ being Element of the carrier of I[01] holds
( g . (b₁,0) = A . b₁ & g . (b₁,1) = B . b₁ & g . (0,b₁) = t1 & g . (1,b₁) = t2 ) ) )
thus g is continuous by A3, PRE_TOPC:26; :: thesis: for b₁ being Element of the carrier of I[01] holds
( g . (b₁,0) = A . b₁ & g . (b₁,1) = B . b₁ & g . (0,b₁) = t1 & g . (1,b₁) = t2 )
( s1 = C . 0 & s2 = C . 1 & t1 = A . 0 & t2 = A . 1 ) by A1, BORSUK_2:def 2;
hence for b₁ being Element of the carrier of I[01] holds
( g . (b₁,0) = A . b₁ & g . (b₁,1) = B . b₁ & g . (0,b₁) = t1 & g . (1,b₁) = t2 ) by A2, A4; :: thesis: verum