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:61
.= Z by A1, XBOOLE_1:28 ; :: thesis: verum