let A be set ; :: thesis: for x, z being object st x in A holds

(A --> z) . x = z

let x, z be object ; :: 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:87;

hence (A --> z) . x = z by FUNCT_1:1; :: thesis: verum

(A --> z) . x = z

let x, z be object ; :: 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:87;

hence (A --> z) . x = z by FUNCT_1:1; :: thesis: verum