for x, y being Element of F_Complex holds
( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) ) by COMPLEX1:8;