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