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 11;
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 11
.= (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 11
.= (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 11
.= s1 ; :: 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 11
.= s2 ; :: thesis: verum