let A be non empty 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:2;
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:32; :: thesis: verum