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
A1: P . 0 = a and
A2: P . 1 = b ; :: thesis: ( (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 0 = b & (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 1 = a )
set e = L[01] (0 ,1 (#) ),((#) 0 ,1);
A3: (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:12
.= 1 by TREAL_1:def 2 ;
A4: (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:12
.= 0 by TREAL_1:def 1 ;
A5: the carrier of (Closed-Interval-TSpace 0 ,1) = [.0 ,1.] by TOPMETR:25;
0 in [.0 ,1.] by XXREAL_1:1;
hence (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 0 = b by A2, A3, A5, FUNCT_2:21; :: thesis: (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 1 = a
1 in [.0 ,1.] by XXREAL_1:1;
hence (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 1 = a by A1, A4, A5, FUNCT_2:21; :: thesis: verum