let T be non empty TopStruct ; :: thesis: for c1, c2 being with_endpoints Curve of T st c1,c2 are_homotopic holds
( the_first_point_of c1 = the_first_point_of c2 & the_last_point_of c1 = the_last_point_of c2 )
let c1, c2 be with_endpoints Curve of T; :: thesis: ( c1,c2 are_homotopic implies ( the_first_point_of c1 = the_first_point_of c2 & the_last_point_of c1 = the_last_point_of c2 ) )
assume c1,c2 are_homotopic ; :: thesis: ( the_first_point_of c1 = the_first_point_of c2 & the_last_point_of c1 = the_last_point_of c2 )
then consider a, b being Point of T, p1, p2 being Path of a,b such that
A1: ( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) ;
A2: ( 0 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:40, XXREAL_1:1;
consider f being Function of [:I[01],I[01]:],T such that
A3: ( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = p1 . t & f . (t,1) = p2 . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A1;
A4: ( f . (0,0) = p1 . 0 & f . (0,1) = p2 . 0 & f . (0,0) = a & f . (0,1) = a ) by A3, A2;
A5: ( f . (1,0) = p1 . 1 & f . (1,1) = p2 . 1 & f . (1,0) = b & f . (1,1) = b ) by A3, A2;
A6: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
A7: dom (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) = the carrier of (Closed-Interval-TSpace (0,1)) by FUNCT_2:def 1
.= [.0,1.] by TOPMETR:18 ;
A8: dom (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) = the carrier of (Closed-Interval-TSpace (0,1)) by FUNCT_2:def 1
.= [.0,1.] by TOPMETR:18 ;
A9: inf (dom c1) <= sup (dom c1) by XXREAL_2:40;
A10: inf (dom c2) <= sup (dom c2) by XXREAL_2:40;
A11: (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) . 0 = ((((sup (dom c2)) - (inf (dom c2))) / (1 - 0)) * (0 - 0)) + (inf (dom c2)) by A10, BORSUK_6:35
.= inf (dom c2) ;
(L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) . 0 = ((((sup (dom c1)) - (inf (dom c1))) / (1 - 0)) * (0 - 0)) + (inf (dom c1)) by A9, BORSUK_6:35
.= inf (dom c1) ;
then p1 . 0 = c1 . (inf (dom c1)) by A1, A6, A7, FUNCT_1:13;
hence the_first_point_of c1 = the_first_point_of c2 by A4, A1, A11, A6, A8, FUNCT_1:13; :: thesis: the_last_point_of c1 = the_last_point_of c2
A12: (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) . 1 = ((((sup (dom c2)) - (inf (dom c2))) / (1 - 0)) * (1 - 0)) + (inf (dom c2)) by A10, BORSUK_6:35
.= sup (dom c2) ;
(L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) . 1 = ((((sup (dom c1)) - (inf (dom c1))) / (1 - 0)) * (1 - 0)) + (inf (dom c1)) by A9, BORSUK_6:35
.= sup (dom c1) ;
then p1 . 1 = c1 . (sup (dom c1)) by A1, A6, A7, FUNCT_1:13;
hence the_last_point_of c1 = the_last_point_of c2 by A5, A1, A12, A6, A8, FUNCT_1:13; :: thesis: verum