let T be non empty convex SubSpace of R^1 ; :: thesis: for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy P,Q) . s,0 = P . s & (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy 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
( (R1Homotopy P,Q) . s,0 = P . s & (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b ) ) )
let P, Q be Path of a,b; :: thesis: for s being Point of I[01] holds
( (R1Homotopy P,Q) . s,0 = P . s & (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b ) ) )
set F = R1Homotopy P,Q;
let s be Point of I[01] ; :: thesis: ( (R1Homotopy P,Q) . s,0 = P . s & (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b ) ) )
A1: ( P . 0[01] = a & Q . 0[01] = a ) by BORSUK_2:def 4;
thus (R1Homotopy P,Q) . s,0 = ((1 - 0 ) * (P . s)) + (0 * (Q . s)) by Def5, BORSUK_1:def 17
.= P . s ; :: thesis: ( (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b ) ) )
thus (R1Homotopy P,Q) . s,1 = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def5, BORSUK_1:def 18
.= Q . s ; :: thesis: for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b )
let t be Point of I[01] ; :: thesis: ( (R1Homotopy P,Q) . 0 ,t = a & (R1Homotopy P,Q) . 1,t = b )
thus (R1Homotopy P,Q) . 0 ,t = ((1 - t) * (P . 0[01] )) + (t * (Q . 0[01] )) by Def5
.= a by A1 ; :: thesis: (R1Homotopy P,Q) . 1,t = b
A2: ( P . 1[01] = b & Q . 1[01] = b ) by BORSUK_2:def 4;
thus (R1Homotopy P,Q) . 1,t = ((1 - t) * (P . 1[01] )) + (t * (Q . 1[01] )) by Def5
.= b by A2 ; :: thesis: verum