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;
take pr2 f ; :: according to BORSUK_2:def 7 :: thesis: ( pr2 f is continuous & ( for b₁ being M3( the carrier of K554()) 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 11;
hence ( pr2 f is continuous & ( for b₁ being M3( the carrier of K554()) 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