:: deftheorem defines Im COMPLSP2:def 3 :
for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i>)) * (z - (z *'));