let A be closed-interval Subset of ; :: thesis: for f being PartFunc of , st A c= dom f holds
f || A is Function of A, REAL
let f be PartFunc of ,; :: thesis: ( A c= dom f implies f || A is Function of A, REAL )
rng f c= REAL ;
then A1: f is Function of dom f, REAL by FUNCT_2:4;
assume A c= dom f ; :: thesis: f || A is Function of A, REAL
hence f || A is Function of A, REAL by A1, FUNCT_2:38; :: thesis: verum