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