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 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
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 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let t1, t2 be 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let l1, l2 be 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let p, q be 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let x, y be 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let f be 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 continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
let g be Homotopy of x,y; ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic implies ( <:f,g:> is continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) )
assume that
A1:
p = pr1 l1
and
A2:
q = pr1 l2
and
A3:
x = pr2 l1
and
A4:
y = pr2 l2
and
A5:
p,q are_homotopic
and
A6:
x,y are_homotopic
; ( <:f,g:> is continuous & ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
set h = <:f,g:>;
( f is continuous & g is continuous )
by A5, A6, BORSUK_6:def 11;
hence
<:f,g:> is continuous
by YELLOW12:41; for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) )
let a be Point of I[01]; ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) )
A7:
dom l1 = the carrier of I[01]
by FUNCT_2:def 1;
A8:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by BORSUK_1:def 2;
A9:
( dom f = the carrier of [:I[01],I[01]:] & dom g = the carrier of [:I[01],I[01]:] )
by FUNCT_2:def 1;
hence <:f,g:> . (a,0) =
[(f . [a,j0]),(g . [a,j0])]
by FUNCT_3:49
.=
[(f . (a,j0)),(g . (a,j0))]
.=
[((pr1 l1) . a),(g . (a,j0))]
by A1, A5, BORSUK_6:def 11
.=
[((pr1 l1) . a),((pr2 l1) . a)]
by A3, A6, BORSUK_6:def 11
.=
[((l1 . a) `1),((pr2 l1) . a)]
by A7, MCART_1:def 12
.=
[((l1 . a) `1),((l1 . a) `2)]
by A7, MCART_1:def 13
.=
l1 . a
by A8, MCART_1:21
;
( <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) )
A10:
dom l2 = the carrier of I[01]
by FUNCT_2:def 1;
thus <:f,g:> . (a,1) =
[(f . [a,j1]),(g . [a,j1])]
by A9, FUNCT_3:49
.=
[(f . (a,j1)),(g . (a,j1))]
.=
[((pr1 l2) . a),(g . (a,j1))]
by A2, A5, BORSUK_6:def 11
.=
[((pr1 l2) . a),((pr2 l2) . a)]
by A4, A6, BORSUK_6:def 11
.=
[((l2 . a) `1),((pr2 l2) . a)]
by A10, MCART_1:def 12
.=
[((l2 . a) `1),((l2 . a) `2)]
by A10, MCART_1:def 13
.=
l2 . a
by A8, MCART_1:21
; for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] )
let b be Point of I[01]; ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] )
thus <:f,g:> . (0,b) =
[(f . [j0,b]),(g . [j0,b])]
by A9, FUNCT_3:49
.=
[(f . (j0,b)),(g . (j0,b))]
.=
[s1,(g . (j0,b))]
by A5, BORSUK_6:def 11
.=
[s1,t1]
by A6, BORSUK_6:def 11
; <:f,g:> . (1,b) = [s2,t2]
thus <:f,g:> . (1,b) =
[(f . [j1,b]),(g . [j1,b])]
by A9, FUNCT_3:49
.=
[(f . (j1,b)),(g . (j1,b))]
.=
[s2,(g . (j1,b))]
by A5, BORSUK_6:def 11
.=
[s2,t2]
by A6, BORSUK_6:def 11
; verum