theorem Th7: :: NOMIN_4:7

for V, A being set
for a being Element of V st A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) holds
for d being TypeSCNominativeData of V,A holds a is_a_value_on d