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 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:90
.= A by A1, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 4; :: thesis: verum