let V, A be set ; 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; ( ( 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
; rng (denaming (V,A,a)) c= A
set f = denaming (V,A,a);
let y be object ; TARSKI:def 3 ( not y in rng (denaming (V,A,a)) or y in A )
assume
y in rng (denaming (V,A,a))
; 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; verum