let V, A be set ; :: thesis: for a being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) holds
rng (denaming (V,A,a)) c= A
let a be Element of V; :: thesis: ( ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) implies rng (denaming (V,A,a)) c= A )
assume A1: for d being TypeSCNominativeData of V,A holds a is_a_value_on d ; :: thesis: rng (denaming (V,A,a)) c= A
set f = denaming (V,A,a);
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (denaming (V,A,a)) or y in A )
assume y in rng (denaming (V,A,a)) ; :: thesis: y in A
then consider x being object such that
A2: x in dom (denaming (V,A,a)) and
A3: (denaming (V,A,a)) . x = y by FUNCT_1:def 3;
dom (denaming (V,A,a)) = { d where d is NonatomicND of V,A : a in dom d } by NOMIN_1:def 18;
then consider d being NonatomicND of V,A such that
A4: x = d and
a in dom d by A2;
a is_a_value_on d by A1;
hence y in A by A3, A4; :: thesis: verum