let n be 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 K634() 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 ) ) )
A1: n in NAT by ORDINAL1:def 13;
then P is continuous ;
hence RealHomotopy (P,Q) is continuous by A1; :: thesis: for b₁ being Element of the carrier of K634() 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 K634() 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 Lm6; :: thesis: verum