set ab = <:(denaming (V,A,a)),(denaming (V,A,b)):>;
set P = op * <:(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 (op * <:(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 (op * <:(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 (op * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= ND (V,A) by A1, XBOOLE_1:1;
rng (op * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= ND (V,A)

proof

for o being object st o in A holds
o in ND (V,A)

proof

let o be object ; :: thesis: ( o in A implies o in ND (V,A) )
assume o in A ; :: thesis: o in ND (V,A)
then o is TypeSCNominativeData of V,A by NOMIN_1:def 6;
hence o in ND (V,A) ; :: thesis: verum

end;

then A c= ND (V,A) by TARSKI:def 3;
hence rng (op * <:(denaming (V,A,a)),(denaming (V,A,b)):>) c= ND (V,A) by XBOOLE_1:1; :: thesis: verum

end;

hence op * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCBinominativeFunction of V,A by A2, RELSET_1:4; :: thesis: verum