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 H being Homotopy of l1,l2
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
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 H being Homotopy of l1,l2
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
let t1, t2 be Point of T; :: thesis: for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
let l1, l2 be Path of [s1,t1],[s2,t2]; :: thesis: for H being Homotopy of l1,l2
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
let H be Homotopy of l1,l2; :: thesis: for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
let p, q be Path of t1,t2; :: thesis: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic implies pr2 H is Homotopy of p,q )
assume A1: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic ) ; :: thesis: pr2 H is Homotopy of p,q
thus p,q are_homotopic :: according to BORSUK_6:def 11 :: thesis: ( pr2 H is continuous & ( for b₁ being M3( the carrier of K554()) holds
( (pr2 H) . (b₁,0) = p . b₁ & (pr2 H) . (b₁,1) = q . b₁ & (pr2 H) . (0,b₁) = t1 & (pr2 H) . (1,b₁) = t2 ) ) )

proof

take pr2 H ; :: according to BORSUK_2:def 7 :: thesis: ( pr2 H is continuous & ( for b₁ being M3( the carrier of K554()) holds
( (pr2 H) . (b₁,0) = p . b₁ & (pr2 H) . (b₁,1) = q . b₁ & (pr2 H) . (0,b₁) = t1 & (pr2 H) . (1,b₁) = t2 ) ) )
thus ( pr2 H is continuous & ( for b₁ being M3( the carrier of K554()) holds
( (pr2 H) . (b₁,0) = p . b₁ & (pr2 H) . (b₁,1) = q . b₁ & (pr2 H) . (0,b₁) = t1 & (pr2 H) . (1,b₁) = t2 ) ) ) by A1, Lm4; :: thesis: verum

end;

thus ( pr2 H is continuous & ( for b₁ being M3( the carrier of K554()) holds
( (pr2 H) . (b₁,0) = p . b₁ & (pr2 H) . (b₁,1) = q . b₁ & (pr2 H) . (0,b₁) = t1 & (pr2 H) . (1,b₁) = t2 ) ) ) by A1, Lm4; :: thesis: verum