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

proof

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

end;

thus ( pr1 H is continuous & ( for b₁ being M3( the carrier of K554()) holds
( (pr1 H) . (b₁,0) = p . b₁ & (pr1 H) . (b₁,1) = q . b₁ & (pr1 H) . (0,b₁) = s1 & (pr1 H) . (1,b₁) = s2 ) ) ) by A1, Lm3; :: thesis: verum