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 17
.= (P . s) + (0 * (Q . s)) by EUCLID:33
.= (P . s) + (0. (TOP-REAL n)) by EUCLID:33
.= P . s by EUCLID:31 ; :: 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 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: 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: n in NAT by ORDINAL1:def 13;
then A2: ( 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 A2, EUCLID:54
.= 1 * a by EUCLID:52
.= a by EUCLID:33 ; :: thesis: (RealHomotopy P,Q) . 1,t = b
A3: ( P . 1[01] = b & Q . 1[01] = b ) by A1, 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 A3, EUCLID:54
.= 1 * b by EUCLID:52
.= b by EUCLID:33 ; :: thesis: verum