theorem :: COMPLSP2:22

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