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