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 that
A1:
( p = pr2 l1 & q = pr2 l2 )
and
A2:
l1,l2 are_homotopic
; :: thesis: pr2 H is Homotopy of p,q
thus
p,q are_homotopic
:: according to BORSUK_6:def 13 :: thesis: ( pr2 H is continuous & ( for b1 being M2(the carrier of K568()) holds
( (pr2 H) . b1,0 = p . b1 & (pr2 H) . b1,1 = q . b1 & (pr2 H) . 0 ,b1 = t1 & (pr2 H) . 1,b1 = t2 ) ) )proof
take
pr2 H
;
:: according to BORSUK_2:def 7 :: thesis: ( pr2 H is continuous & ( for b1 being M2(the carrier of K568()) 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
M2(the
carrier of
K568()) 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, A2, Lm4;
:: thesis: verum
end;
thus
( pr2 H is continuous & ( for b1 being M2(the carrier of K568()) 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, A2, Lm4; :: thesis: verum