let S, T be non empty TopSpace; 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; 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; 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]; 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; 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; ( 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 )
; pr2 H is Homotopy of p,q
thus
p,q are_homotopic
BORSUK_6:def 11 ( pr2 H is continuous & ( for b1 being M3( the carrier of K554()) holds
( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) )
thus
( pr2 H is continuous & ( for b1 being M3( the carrier of K554()) holds
( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) )
by A1, Lm4; verum