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

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