let f be Function; :: thesis: {} is f -compatible
let x be set ; :: according to FUNCT_1:def 14 :: thesis: ( x in dom {} implies {} . x in f . x )
thus ( x in dom {} implies {} . x in f . x ) ; :: thesis: verum