let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b st P is continuous holds
P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T
let a, b be Point of T; :: thesis: for P being Path of a,b st P is continuous holds
P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T
reconsider g = L[01] (((0,1) (#)),((#) (0,1))) as Function of I[01],I[01] by TOPMETR:20;
let P be Path of a,b; :: thesis: ( P is continuous implies P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T )
assume A1: P is continuous ; :: thesis: P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T
reconsider f = P * g as Function of I[01],T ;
g is continuous by TOPMETR:20, TREAL_1:8;
then f is continuous by A1;
hence P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T ; :: thesis: verum