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 H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
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 H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
let t1, t2 be Point of T; :: thesis: for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
let l1, l2 be Path of [s1,t1],[s2,t2]; :: thesis: for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
let H be Homotopy of l1,l2; :: thesis: ( l1,l2 are_homotopic implies ( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) ) )
A1: dom l1 = the carrier of I[01] by FUNCT_2:def 1;
A2: dom l2 = the carrier of I[01] by FUNCT_2:def 1;
assume A3: l1,l2 are_homotopic ; :: thesis: ( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
then H is continuous by BORSUK_6:def 13;
hence pr1 H is continuous by Th9; :: thesis: for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) )
let a be Point of I[01] ; :: thesis: ( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) )
A4: dom H = the carrier of [:I[01] ,I[01] :] by FUNCT_2:def 1;
hence (pr1 H) . a,0 = (H . [a,j0]) `1 by MCART_1:def 12
.= (H . a,j0) `1
.= (l1 . a) `1 by A3, BORSUK_6:def 13
.= (pr1 l1) . a by A1, MCART_1:def 12 ;
:: thesis: ( (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) )
thus (pr1 H) . a,1 = (H . [a,j1]) `1 by A4, MCART_1:def 12
.= (H . a,j1) `1
.= (l2 . a) `1 by A3, BORSUK_6:def 13
.= (pr1 l2) . a by A2, MCART_1:def 12 ; :: thesis: for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 )
let b be Point of I[01] ; :: thesis: ( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 )
thus (pr1 H) . 0 ,b = (H . [j0,b]) `1 by A4, MCART_1:def 12
.= (H . j0,b) `1
.= [s1,t1] `1 by A3, BORSUK_6:def 13
.= s1 by MCART_1:def 1 ; :: thesis: (pr1 H) . 1,b = s2
thus (pr1 H) . 1,b = (H . [j1,b]) `1 by A4, MCART_1:def 12
.= (H . j1,b) `1
.= [s2,t2] `1 by A3, BORSUK_6:def 13
.= s2 by MCART_1:def 1 ; :: thesis: verum