let T be non empty TopStruct ; :: thesis: for c1, c2 being with_endpoints Curve of T
for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )

let c1, c2 be with_endpoints Curve of T; :: thesis: for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )

let a, b be Point of T; :: thesis: for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )

let p1, p2 be Path of a,b; :: thesis: ( c1 = p1 & c2 = p2 & a,b are_connected implies ( c1,c2 are_homotopic iff p1,p2 are_homotopic ) )
assume A1: ( c1 = p1 & c2 = p2 ) ; :: thesis: ( not a,b are_connected or ( c1,c2 are_homotopic iff p1,p2 are_homotopic ) )
assume A2: a,b are_connected ; :: thesis: ( c1,c2 are_homotopic iff p1,p2 are_homotopic )
A3: ( 0 is Point of I & 1 is Point of I ) by ;
A4: ( inf (dom c1) = 0 & sup (dom c1) = 1 & inf (dom c2) = 0 & sup (dom c2) = 1 ) by ;
A5: ( dom p1 = the carrier of I & dom p2 = the carrier of I ) by FUNCT_2:def 1;
thus ( c1,c2 are_homotopic implies p1,p2 are_homotopic ) :: thesis: ( p1,p2 are_homotopic implies c1,c2 are_homotopic )
proof
assume c1,c2 are_homotopic ; :: thesis: p1,p2 are_homotopic
then consider aa, bb being Point of T, pp1, pp2 being Path of aa,bb such that
A6: ( pp1 = c1 * (L (0,1,(inf (dom c1)),(sup (dom c1)))) & pp2 = c2 * (L (0,1,(inf (dom c2)),(sup (dom c2)))) & pp1,pp2 are_homotopic ) ;
consider f being Function of ,T such that
A7: ( f is continuous & ( for t being Point of I holds
( f . (t,0) = pp1 . t & f . (t,1) = pp2 . t & f . (0,t) = aa & f . (1,t) = bb ) ) ) by A6;
A8: ( pp1 = p1 & pp2 = p2 ) by ;
A9: ( f . (0,0) = pp1 . 0 & f . (0,1) = pp2 . 0 & f . (0,0) = aa & f . (0,1) = aa ) by A7, A3;
A10: ( f . (1,0) = pp1 . 1 & f . (1,1) = pp2 . 1 & f . (1,0) = bb & f . (1,1) = bb ) by A7, A3;
( aa = a & bb = b ) by ;
hence p1,p2 are_homotopic by A7, A8; :: thesis: verum
end;
assume A11: p1,p2 are_homotopic ; :: thesis: c1,c2 are_homotopic
( p1 = p1 * (L (0,1,0,1)) & p2 = p2 * (L (0,1,0,1)) ) by ;
hence c1,c2 are_homotopic by A4, A1, A11; :: thesis: verum