for z being FinSequence of COMPLEX holds (z *') *' = z ;