let n be Element of NAT ; :: thesis: 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
for s being Point of I[01] holds
( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
reconsider x0 = 0 , x1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
let a, b be Point of T; :: thesis: for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
let P, Q be Path of a,b; :: thesis: for s being Point of I[01] holds
( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
set F = ConvexHomotopy P,Q;
let s be Point of I[01] ; :: thesis: ( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:55;
A1: P . x0 = a by BORSUK_2:def 4;
(ConvexHomotopy P,Q) . s,x0 = ((1 - x0) * a1) + (x0 * b1) by Def2;
hence (ConvexHomotopy P,Q) . s,0 = a1 + (0 * b1) by EUCLID:33
.= a1 + (0. (TOP-REAL n)) by EUCLID:33
.= P . s by EUCLID:31 ;
:: thesis: ( (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
(ConvexHomotopy P,Q) . s,x1 = ((1 - x1) * a1) + (x1 * b1) by Def2;
hence (ConvexHomotopy P,Q) . s,1 = (0. (TOP-REAL n)) + (1 * b1) by EUCLID:33
.= (0. (TOP-REAL n)) + b1 by EUCLID:33
.= Q . s by EUCLID:31 ;
:: thesis: for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b )
reconsider a1 = P . x0, b1 = Q . x0 as Point of (TOP-REAL n) by PRE_TOPC:55;
let t be Point of I[01] ; :: thesis: ( (ConvexHomotopy P,Q) . 0 ,t = a & (ConvexHomotopy P,Q) . 1,t = b )
( (ConvexHomotopy P,Q) . 0 ,t = ((1 - t) * a1) + (t * b1) & Q . x0 = a ) by Def2, BORSUK_2:def 4;
hence (ConvexHomotopy P,Q) . 0 ,t = ((1 * a1) - (t * a1)) + (t * a1) by A1, EUCLID:54
.= 1 * a1 by EUCLID:52
.= a by A1, EUCLID:33 ;
:: thesis: (ConvexHomotopy P,Q) . 1,t = b
A2: Q . x1 = b by BORSUK_2:def 4;
reconsider a1 = P . x1, b1 = Q . x1 as Point of (TOP-REAL n) by PRE_TOPC:55;
A3: P . x1 = b by BORSUK_2:def 4;
(ConvexHomotopy P,Q) . 1,t = ((1 - t) * a1) + (t * b1) by Def2;
hence (ConvexHomotopy P,Q) . 1,t = ((1 * a1) - (t * b1)) + (t * a1) by A3, A2, EUCLID:54
.= 1 * b1 by A3, A2, EUCLID:52
.= b by A2, EUCLID:33 ;
:: thesis: verum