let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st A c= dom f holds
f || A is Function of A,REAL
let f be PartFunc of REAL ,REAL ; :: 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