:: deftheorem defines Re COMPLSP2:def 2 :
for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *'));