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 holds P,Q are_homotopic
let a, b be Point of T; for P, Q being Path of a,b holds P,Q are_homotopic
let P, Q be Path of a,b; P,Q are_homotopic
take F = R1Homotopy (P,Q); BORSUK_2:def 7 ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) )
thus
F is continuous
by Lm8; for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b )
thus
for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b )
by Lm9; verum