let V, A be set ; :: thesis: 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
let a be Element of V; :: thesis: ( A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) implies for d being TypeSCNominativeData of V,A holds a is_a_value_on d )
assume that
A1: COMPLEX c= A and
A2: for d being TypeSCNominativeData of V,A holds a is_complex_on d ; :: according to NOMIN_4:def 1 :: thesis: for d being TypeSCNominativeData of V,A holds a is_a_value_on d
let d be TypeSCNominativeData of V,A; :: thesis: a is_a_value_on d
a is_complex_on d by A2;
then (denaming (V,A,a)) . d in COMPLEX by XCMPLX_0:def 2;
hence (denaming (V,A,a)) . d in A by A1; :: according to NOMIN_4:def 6 :: thesis: verum