let n be Nat; :: thesis: 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); :: thesis: for P, Q being Path of a,b holds P,Q are_homotopic
let P, Q be Path of a,b; :: thesis: P,Q are_homotopic
take F = RealHomotopy P,Q; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b₁ being Element of the carrier of K633() holds
( F . b₁,0 = P . b₁ & F . b₁,1 = Q . b₁ & F . 0 ,b₁ = a & F . 1,b₁ = b ) ) )
A1: n in NAT by ORDINAL1:def 13;
then P is continuous ;
hence F is continuous by A1, Lm5; :: thesis: for b₁ being Element of the carrier of K633() holds
( F . b₁,0 = P . b₁ & F . b₁,1 = Q . b₁ & F . 0 ,b₁ = a & F . 1,b₁ = b )
thus for b₁ being Element of the carrier of K633() holds
( F . b₁,0 = P . b₁ & F . b₁,1 = Q . b₁ & F . 0 ,b₁ = a & F . 1,b₁ = b ) by Lm6; :: thesis: verum