let Y be set ; :: thesis: for f being Function holds dom (Y | f) c= dom f
let f be Function; :: thesis: dom (Y | f) c= dom f
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Y | f) or x in dom f )
thus ( not x in dom (Y | f) or x in dom f ) by Th85; :: thesis: verum