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 t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
p,q 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 t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
p,q 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 t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
p,q are_homotopic
let l1, l2 be Path of [s1,t1],[s2,t2]; :: thesis: for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
p,q are_homotopic
let p, q be Path of t1,t2; :: thesis: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic implies p,q are_homotopic )
assume that
A1: ( p = pr2 l1 & q = pr2 l2 ) and
A2: l1,l2 are_homotopic ; :: thesis: p,q are_homotopic
consider f being Function of [:I[01] ,I[01] :],[:S,T:] such that
A3: ( f is continuous & ( for a being Point of I[01] holds
( f . a,0 = l1 . a & f . a,1 = l2 . a & ( for b being Point of I[01] holds
( f . 0 ,b = [s1,t1] & f . 1,b = [s2,t2] ) ) ) ) ) by A2, BORSUK_2:def 7;
take pr2 f ; :: according to BORSUK_2:def 7 :: thesis: ( pr2 f is continuous & ( for b₁ being M2(the carrier of K568()) holds
( (pr2 f) . b₁,0 = p . b₁ & (pr2 f) . b₁,1 = q . b₁ & (pr2 f) . 0 ,b₁ = t1 & (pr2 f) . 1,b₁ = t2 ) ) )
f is Homotopy of l1,l2 by A2, A3, BORSUK_6:def 13;
hence ( pr2 f is continuous & ( for b₁ being M2(the carrier of K568()) holds
( (pr2 f) . b₁,0 = p . b₁ & (pr2 f) . b₁,1 = q . b₁ & (pr2 f) . 0 ,b₁ = t1 & (pr2 f) . 1,b₁ = t2 ) ) ) by A1, A2, Lm4; :: thesis: verum