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[01] & 1 is Point of I[01] ) by BORSUK_1:40, XXREAL_1:1;

A4: ( inf (dom c1) = 0 & sup (dom c1) = 1 & inf (dom c2) = 0 & sup (dom c2) = 1 ) by A1, Th4;

A5: ( dom p1 = the carrier of I[01] & dom p2 = the carrier of I[01] ) 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 )

( p1 = p1 * (L[01] (0,1,0,1)) & p2 = p2 * (L[01] (0,1,0,1)) ) by A5, Th1, RELAT_1:52, TOPMETR:20;

hence c1,c2 are_homotopic by A4, A1, A11; :: thesis: verum

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[01] & 1 is Point of I[01] ) by BORSUK_1:40, XXREAL_1:1;

A4: ( inf (dom c1) = 0 & sup (dom c1) = 1 & inf (dom c2) = 0 & sup (dom c2) = 1 ) by A1, Th4;

A5: ( dom p1 = the carrier of I[01] & dom p2 = the carrier of I[01] ) 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 A11:
p1,p2 are_homotopic
; :: thesis: c1,c2 are_homotopic
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[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & pp2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & pp1,pp2 are_homotopic ) ;

consider f being Function of [:I[01],I[01]:],T such that

A7: ( f is continuous & ( for t being Point of I[01] 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 A1, A6, A4, A5, Th1, RELAT_1:52, TOPMETR:20;

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 A8, A9, A10, A2, BORSUK_2:def 2;

hence p1,p2 are_homotopic by A7, A8; :: thesis: verum

end;then consider aa, bb being Point of T, pp1, pp2 being Path of aa,bb such that

A6: ( pp1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & pp2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & pp1,pp2 are_homotopic ) ;

consider f being Function of [:I[01],I[01]:],T such that

A7: ( f is continuous & ( for t being Point of I[01] 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 A1, A6, A4, A5, Th1, RELAT_1:52, TOPMETR:20;

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 A8, A9, A10, A2, BORSUK_2:def 2;

hence p1,p2 are_homotopic by A7, A8; :: thesis: verum

( p1 = p1 * (L[01] (0,1,0,1)) & p2 = p2 * (L[01] (0,1,0,1)) ) by A5, Th1, RELAT_1:52, TOPMETR:20;

hence c1,c2 are_homotopic by A4, A1, A11; :: thesis: verum