let A, x, z be set ; :: thesis: ( x in A implies (A --> z) . x = z )
assume A1: x in A ; :: thesis: (A --> z) . x = z
z in {z} by TARSKI:def 1;
then [x,z] in A --> z by A1, ZFMISC_1:106;
hence (A --> z) . x = z by FUNCT_1:8; :: thesis: verum