let S, T be non empty TopSpace; :: thesis: for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
l1,l2 are_homotopic
let s1, s2 be Point of S; :: thesis: for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
l1,l2 are_homotopic
let t1, t2 be Point of T; :: thesis: for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
l1,l2 are_homotopic
let l1, l2 be Path of [s1,t1],[s2,t2]; :: thesis: for p, q being Path of s1,s2
for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
l1,l2 are_homotopic
let p, q be Path of s1,s2; :: thesis: for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
l1,l2 are_homotopic
let x, y be Path of t1,t2; :: thesis: ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic implies l1,l2 are_homotopic )
assume that
A1: ( p = pr1 l1 & q = pr1 l2 ) and
A2: ( x = pr2 l1 & y = pr2 l2 ) and
A3: p,q are_homotopic and
A4: x,y are_homotopic ; :: thesis: l1,l2 are_homotopic
consider g being Function of [:I[01],I[01]:],T such that
A5: ( g is continuous & ( for a being Point of I[01] holds
( g . (a,0) = (pr2 l1) . a & g . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds
( g . (0,b) = t1 & g . (1,b) = t2 ) ) ) ) ) by A2, A4;
A6: g is Homotopy of x,y by A2, A4, A5, BORSUK_6:def 11;
consider f being Function of [:I[01],I[01]:],S such that
A7: ( f is continuous & ( for a being Point of I[01] holds
( f . (a,0) = (pr1 l1) . a & f . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds
( f . (0,b) = s1 & f . (1,b) = s2 ) ) ) ) ) by A1, A3;
take <:f,g:> ; :: according to BORSUK_2:def 7 :: thesis: ( <:f,g:> is continuous & ( for b₁ being M3( the carrier of K554()) holds
( <:f,g:> . (b₁,0) = l1 . b₁ & <:f,g:> . (b₁,1) = l2 . b₁ & <:f,g:> . (0,b₁) = [s1,t1] & <:f,g:> . (1,b₁) = [s2,t2] ) ) )
f is Homotopy of p,q by A1, A3, A7, BORSUK_6:def 11;
hence ( <:f,g:> is continuous & ( for b₁ being M3( the carrier of K554()) holds
( <:f,g:> . (b₁,0) = l1 . b₁ & <:f,g:> . (b₁,1) = l2 . b₁ & <:f,g:> . (0,b₁) = [s1,t1] & <:f,g:> . (1,b₁) = [s2,t2] ) ) ) by A1, A2, A3, A4, A6, Lm5; :: thesis: verum