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

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