let n be Nat; :: thesis: for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b
for s being Point of I[01] holds
( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
let a, b be Point of (TOP-REAL n); :: thesis: for P, Q being Path of a,b
for s being Point of I[01] holds
( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
let P, Q be Path of a,b; :: thesis: for s being Point of I[01] holds
( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
set F = RealHomotopy (P,Q);
let s be Point of I[01]; :: thesis: ( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
thus (RealHomotopy (P,Q)) . (s,0) = ((1 - 0) * (P . s)) + (0 * (Q . s)) by Def7, BORSUK_1:def 14
.= (P . s) + (0 * (Q . s)) by RLVECT_1:def 8
.= (P . s) + (0. (TOP-REAL n)) by RLVECT_1:10
.= P . s by RLVECT_1:4 ; :: thesis: ( (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
thus (RealHomotopy (P,Q)) . (s,1) = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def7, BORSUK_1:def 15
.= (0. (TOP-REAL n)) + (1 * (Q . s)) by RLVECT_1:10
.= (0. (TOP-REAL n)) + (Q . s) by RLVECT_1:def 8
.= Q . s by RLVECT_1:4 ; :: thesis: for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b )
let t be Point of I[01]; :: thesis: ( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b )
A1: ( P . 0[01] = a & Q . 0[01] = a ) by BORSUK_2:def 4;
thus (RealHomotopy (P,Q)) . (0,t) = ((1 - t) * (P . 0[01])) + (t * (Q . 0[01])) by Def7
.= ((1 * a) - (t * a)) + (t * a) by A1, RLVECT_1:35
.= 1 * a by RLVECT_4:1
.= a by RLVECT_1:def 8 ; :: thesis: (RealHomotopy (P,Q)) . (1,t) = b
A2: ( P . 1[01] = b & Q . 1[01] = b ) by BORSUK_2:def 4;
thus (RealHomotopy (P,Q)) . (1,t) = ((1 - t) * (P . 1[01])) + (t * (Q . 1[01])) by Def7
.= ((1 * b) - (t * b)) + (t * b) by A2, RLVECT_1:35
.= 1 * b by RLVECT_4:1
.= b by RLVECT_1:def 8 ; :: thesis: verum