let x, y, A be set ; :: thesis: ( x in A implies (x .--> y) | A = x .--> y )
assume x in A ; :: thesis: (x .--> y) | A = x .--> y
then dom (x .--> y) c= A by ZFMISC_1:31;
hence (x .--> y) | A = x .--> y by RELAT_1:68; :: thesis: verum