let A be set ; :: thesis: for C being non empty set
for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
let C be non empty set ; :: thesis: for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
let B be Subset of A; :: thesis: for g being Function of A,C holds dom (g | B) = B
let g be Function of A,C; :: thesis: dom (g | B) = B
thus dom (g | B) = (dom g) /\ B by RELAT_1:61
.= A /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28 ; :: thesis: verum