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
rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:]
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 rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:] )
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
A1: rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:(rng (denaming (V,A,a))),(rng (denaming (V,A,b))):] by FUNCT_3:51;
assume ( ( 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: rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:]
then ( rng (denaming (V,A,a)) c= A & rng (denaming (V,A,b)) c= A ) by Th8;
then [:(rng (denaming (V,A,a))),(rng (denaming (V,A,b))):] c= [:A,A:] by ZFMISC_1:96;
hence rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:] by A1, XBOOLE_1:1; :: thesis: verum