for n being Element of NAT holds the carrier of (the_Complex_Space n) = COMPLEX n ;