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

(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