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 total
let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f implies f || A is total )
assume A1: A c= dom f ; :: thesis: f || A is total
dom (f || A) = (dom f) /\ A by RELAT_1:61
.= A by A1, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 2; :: thesis: verum