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
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 g = L[01] (0 ,1 (#) ),((#) 0 ,1) as Function of I[01] ,I[01] by TOPMETR:27;
reconsider f = P * g as Function of I[01] ,T ;
g is continuous by TOPMETR:27, TREAL_1:11;
then f is continuous by A1;
hence P * (L[01] (0 ,1 (#) ),((#) 0 ,1)) is continuous Function of I[01] ,T ; :: thesis: verum