( dom (x .--> a) = {x} & rng (x .--> a) = {a} ) by FUNCOP_1:14, FUNCOP_1:19;
hence a | is Val_Sub of A by RELSET_1:11; :: thesis: verum