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

proof

take <:f,g:> ; :: according to BORSUK_2:def 7 :: thesis: ( <:f,g:> is continuous & ( for b₁ being M3( the carrier of K554()) holds
( <:f,g:> . (b₁,0) = l1 . b₁ & <:f,g:> . (b₁,1) = l2 . b₁ & <:f,g:> . (0,b₁) = [s1,t1] & <:f,g:> . (1,b₁) = [s2,t2] ) ) )
thus ( <:f,g:> is continuous & ( for b₁ being M3( the carrier of K554()) holds
( <:f,g:> . (b₁,0) = l1 . b₁ & <:f,g:> . (b₁,1) = l2 . b₁ & <:f,g:> . (0,b₁) = [s1,t1] & <:f,g:> . (1,b₁) = [s2,t2] ) ) ) by A1, Lm5; :: thesis: verum

end;

thus ( <:f,g:> is continuous & ( for b₁ being M3( the carrier of K554()) holds
( <:f,g:> . (b₁,0) = l1 . b₁ & <:f,g:> . (b₁,1) = l2 . b₁ & <:f,g:> . (0,b₁) = [s1,t1] & <:f,g:> . (1,b₁) = [s2,t2] ) ) ) by A1, Lm5; :: thesis: verum