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, BORSUK_2:def 7;
A6: g is Homotopy of x,y by A2, A4, A5, BORSUK_6:def 13;
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, BORSUK_2:def 7;
take <:f,g:> ; :: according to BORSUK_2:def 7 :: thesis: ( <:f,g:> is continuous & ( for b₁ being M2(the carrier of K573()) 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 13;
hence ( <:f,g:> is continuous & ( for b₁ being M2(the carrier of K573()) 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