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