let n be Element of NAT ; :: thesis:
let a, b be Point of (TOP-REAL n); :: thesis:
let P, Q be Path of a,b; :: thesis:
set F = RealHomotopy P,Q;
let s be Point of I[01] ; :: thesis:
thus (RealHomotopy P,Q) . s,0 = ((1 - 0 ) * (P . s)) + (0 * (Q . s)) by Def5, BORSUK_1:def 17
.= (P . s) + (0 * (Q . s)) by EUCLID:33
.= (P . s) + (0. (TOP-REAL n)) by EUCLID:33
.= P . s by EUCLID:31 ; :: thesis:
thus (RealHomotopy P,Q) . s,1 = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def5, BORSUK_1:def 18
.= (0. (TOP-REAL n)) + (1 * (Q . s)) by EUCLID:33
.= (0. (TOP-REAL n)) + (Q . s) by EUCLID:33
.= Q . s by EUCLID:31 ; :: thesis:
let t be Point of I[01] ; :: thesis:
A1: P . 0[01] = a by BORSUK_2:def 4;
A2: Q . 0[01] = a by BORSUK_2:def 4;
A3: P . 1[01] = b by BORSUK_2:def 4;
A4: Q . 1[01] = b by BORSUK_2:def 4;
thus (RealHomotopy P,Q) . 0 ,t = ((1 - t) * (P . 0[01] )) + (t * (Q . 0[01] )) by Def5
.= ((1 * a) - (t * a)) + (t * a) by A1, A2, EUCLID:54
.= 1 * a by EUCLID:52
.= a by EUCLID:33 ; :: thesis:
thus (RealHomotopy P,Q) . 1,t = ((1 - t) * (P . 1[01] )) + (t * (Q . 1[01] )) by Def5
.= ((1 * b) - (t * b)) + (t * b) by A3, A4, EUCLID:54
.= 1 * b by EUCLID:52
.= b by EUCLID:33 ; :: thesis: