let T be non empty interval SubSpace of R^1 ; 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; 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; 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]; ( (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 Def4, BORSUK_1:def 14
.=
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 ) ) )
thus (R1Homotopy (P,Q)) . (s,1) =
((1 - 1) * (P . s)) + (1 * (Q . s))
by Def4, BORSUK_1:def 15
.=
Q . s
; 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]; ( (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 Def4
.=
a
by A1
; (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 Def4
.=
b
by A2
; verum