:: deftheorem defines is_complex_on NOMIN_4:def 5 :
for V, A being set
for d being TypeSCNominativeData of V,A
for a being Element of V holds
( a is_complex_on d iff (denaming (V,A,a)) . d is complex );