let A, C be set ; :: thesis: for f being Function of A,C holds {f} is FUNCTION_DOMAIN of A,C
let f be Function of A,C; :: thesis: {f} is FUNCTION_DOMAIN of A,C
A1: {f} is non empty functional set by Th8;
for g being Element of {f} holds g is Function of A,C by TARSKI:def 1;
hence {f} is FUNCTION_DOMAIN of A,C by A1, Def2; :: thesis: verum