let n be Element of NAT ; :: thesis: for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds RealHomotopy P,Q is Homotopy of P,Q
let a, b be Point of (TOP-REAL n); :: thesis: for P, Q being Path of a,b holds RealHomotopy P,Q is Homotopy of P,Q
let P, Q be Path of a,b; :: thesis: RealHomotopy P,Q is Homotopy of P,Q
thus P,Q are_homotopic by Th60; :: according to BORSUK_6:def 13 :: thesis: ( RealHomotopy P,Q is continuous & ( for b₁ being Element of the carrier of K630() holds
( (RealHomotopy P,Q) . b₁,0 = P . b₁ & (RealHomotopy P,Q) . b₁,1 = Q . b₁ & (RealHomotopy P,Q) . 0 ,b₁ = a & (RealHomotopy P,Q) . 1,b₁ = b ) ) )
thus RealHomotopy P,Q is continuous ; :: thesis: for b₁ being Element of the carrier of K630() holds
( (RealHomotopy P,Q) . b₁,0 = P . b₁ & (RealHomotopy P,Q) . b₁,1 = Q . b₁ & (RealHomotopy P,Q) . 0 ,b₁ = a & (RealHomotopy P,Q) . 1,b₁ = b )
thus for b₁ being Element of the carrier of K630() holds
( (RealHomotopy P,Q) . b₁,0 = P . b₁ & (RealHomotopy P,Q) . b₁,1 = Q . b₁ & (RealHomotopy P,Q) . 0 ,b₁ = a & (RealHomotopy P,Q) . 1,b₁ = b ) by Lm5; :: thesis: verum