let V, A be set ; :: thesis: for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds
dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
let a, b be Element of V; :: thesis: ( ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) implies dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) )
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
assume A1: ( ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) ) ; :: thesis: dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
dom (Equality A) = [:A,A:] by FUNCT_2:def 1;
then rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= dom (Equality A) by A1, Th9;
then dom (Equality (A,a,b)) = dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by RELAT_1:27;
hence dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by FUNCT_3:def 7; :: thesis: verum