let n be Nat; for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds P,Q are_homotopic
let a, b be Point of (TOP-REAL n); 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 = RealHomotopy (P,Q); BORSUK_2:def 7 ( F is continuous & ( for b1 being Element of the carrier of K512() holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) )
thus
F is continuous
by Lm5; for b1 being Element of the carrier of K512() 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 K512() holds
( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b )
by Lm6; verum