for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )