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