let A be set ; :: thesis: for x, y being object st not x in A holds
(x .--> y) | A = {}
let x, y be object ; :: thesis: ( not x in A implies (x .--> y) | A = {} )
assume not x in A ; :: thesis: (x .--> y) | A = {}
then dom (x .--> y) misses A by ZFMISC_1:50;
hence (x .--> y) | A = {} by RELAT_1:66; :: thesis: verum