set ab = <:(denaming (V,A,a)),(denaming (V,A,b)):>;
set P = p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;
A1: dom <:(denaming (V,A,a)),(denaming (V,A,b)):> = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by FUNCT_3:def 7;
for o being object st o in dom (p * <:(denaming (V,A,a)),(denaming (V,A,b)):>) holds
o in dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by FUNCT_1:11;
then dom (p * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by TARSKI:def 3;
then A2: dom (p * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= ND (V,A) by A1, XBOOLE_1:1;
rng (p * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= BOOLEAN ;
hence p * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCPartialNominativePredicate of V,A by A2, RELSET_1:4; :: thesis: verum