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 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; :: 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 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; :: 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 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]; :: 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 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; :: 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 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; :: 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 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; :: 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 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; :: 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 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 ; :: thesis: ( <: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; :: thesis: 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]; :: thesis: ( <: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 ;
:: thesis: ( <: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 ; :: thesis: 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]; :: thesis: ( <: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 ; :: thesis: <: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 ; :: thesis: verum