let f be Relation; :: thesis: for X being set st X misses dom f holds
f | X = {}
let X be set ; :: thesis: ( X misses dom f implies f | X = {} )
assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f | X = {}
thus f | X = (f | (dom f)) | X
.= f | {} by A1, Th65
.= {} ; :: thesis: verum