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

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