let S, T be non empty TopSpace; :: thesis:
let s1, s2 be Point of S; :: thesis:
let t1, t2 be Point of T; :: thesis:
let l1, l2 be Path of [s1,t1],[s2,t2]; :: thesis:
let H be Homotopy of l1,l2; :: thesis:
assume A1: l1,l2 are_homotopic ; :: thesis:
then H is continuous by BORSUK_6:def 13;
hence pr2 H is continuous by Th10; :: thesis:
let a be Point of I[01] ; :: thesis:
A2: dom H = the carrier of [:I[01] ,I[01] :] by FUNCT_2:def 1;
A3: dom l1 = the carrier of I[01] by FUNCT_2:def 1;
A4: dom l2 = the carrier of I[01] by FUNCT_2:def 1;
thus (pr2 H) . a,0 = (H . [a,j0]) `2 by A2, MCART_1:def 13
.= (H . a,j0) `2
.= (l1 . a) `2 by A1, BORSUK_6:def 13
.= (pr2 l1) . a by A3, MCART_1:def 13 ; :: thesis:
thus (pr2 H) . a,1 = (H . [a,j1]) `2 by A2, MCART_1:def 13
.= (H . a,j1) `2
.= (l2 . a) `2 by A1, BORSUK_6:def 13
.= (pr2 l2) . a by A4, MCART_1:def 13 ; :: thesis:
let b be Point of I[01] ; :: thesis:
thus (pr2 H) . 0 ,b = (H . [j0,b]) `2 by A2, MCART_1:def 13
.= (H . j0,b) `2
.= [s1,t1] `2 by A1, BORSUK_6:def 13
.= t1 by MCART_1:def 2 ; :: thesis:
thus (pr2 H) . 1,b = (H . [j1,b]) `2 by A2, MCART_1:def 13
.= (H . j1,b) `2
.= [s2,t2] `2 by A1, BORSUK_6:def 13
.= t2 by MCART_1:def 2 ; :: thesis: