theorem :: COMPLSP1:3

for n being Element of NAT
for p being Point of (the_Complex_Space n) holds p is Element of COMPLEX n ;