let A be set ; :: thesis: for x being object holds (A --> x) " {x} = A
let x be object ; :: thesis: (A --> x) " {x} = A
x in {x} by TARSKI:def 1;
hence (A --> x) " {x} = A by Th14; :: thesis: verum