let n be Element of NAT ; for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let T be non empty convex SubSpace of TOP-REAL n; for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let a, b be Point of T; for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q
let P, Q be Path of a,b; ConvexHomotopy (P,Q) is Homotopy of P,Q
thus
P,Q are_homotopic
by Th2; BORSUK_6:def 11 ( ConvexHomotopy (P,Q) is continuous & ( for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) ) )
thus
ConvexHomotopy (P,Q) is continuous
; for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b )
thus
for b1 being Element of the carrier of I[01] holds
( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b )
by Lm6; verum