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 13;
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 5;
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:69
.= [(f . a,j0),(g . a,j0)]
.= [((pr1 l1) . a),(g . a,j0)] by A1, A5, BORSUK_6:def 13
.= [((pr1 l1) . a),((pr2 l1) . a)] by A3, A6, BORSUK_6:def 13
.= [((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:23 ;
:: 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:69
.= [(f . a,j1),(g . a,j1)]
.= [((pr1 l2) . a),(g . a,j1)] by A2, A5, BORSUK_6:def 13
.= [((pr1 l2) . a),((pr2 l2) . a)] by A4, A6, BORSUK_6:def 13
.= [((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:23 ; :: 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:69
.= [(f . j0,b),(g . j0,b)]
.= [s1,(g . j0,b)] by A5, BORSUK_6:def 13
.= [s1,t1] by A6, BORSUK_6:def 13 ; :: thesis: <:f,g:> . 1,b = [s2,t2]
thus <:f,g:> . 1,b = [(f . [j1,b]),(g . [j1,b])] by A9, FUNCT_3:69
.= [(f . j1,b),(g . j1,b)]
.= [s2,(g . j1,b)] by A5, BORSUK_6:def 13
.= [s2,t2] by A6, BORSUK_6:def 13 ; :: thesis: verum