A1: 0 in [.0,1.] by XXREAL_1:1;
set e = L[01] (((0,1) (#)),((#) (0,1)));
let X be non empty TopStruct ; :: thesis: for a, b being Point of X
for P being Path of a,b st P . 0 = a & P . 1 = b holds
( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )
let a, b be Point of X; :: thesis: for P being Path of a,b st P . 0 = a & P . 1 = b holds
( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )
let P be Path of a,b; :: thesis: ( P . 0 = a & P . 1 = b implies ( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a ) )
assume that
A2: P . 0 = a and
A3: P . 1 = b ; :: thesis: ( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )
A4: the carrier of (Closed-Interval-TSpace (0,1)) = [.0,1.] by TOPMETR:18;
(L[01] (((0,1) (#)),((#) (0,1)))) . 0 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) by TREAL_1:def 1
.= (0,1) (#) by TREAL_1:9
.= 1 by TREAL_1:def 2 ;
hence (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b by A3, A4, A1, FUNCT_2:15; :: thesis: (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a
A5: 1 in [.0,1.] by XXREAL_1:1;
(L[01] (((0,1) (#)),((#) (0,1)))) . 1 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) by TREAL_1:def 2
.= (#) (0,1) by TREAL_1:9
.= 0 by TREAL_1:def 1 ;
hence (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a by A2, A4, A5, FUNCT_2:15; :: thesis: verum