let Z be open Subset of REAL ; :: thesis: for f being Function of REAL ,REAL holds dom (f | Z) = Z
let f be Function of REAL ,REAL ; :: thesis: dom (f | Z) = Z
A1: dom f = REAL by FUNCT_2:def 1;
thus dom (f | Z) = (dom f) /\ Z by RELAT_1:90
.= Z by A1, XBOOLE_1:28 ; :: thesis: verum