theorem Lm46: :: ALGNUM_1:37

for x, z1, z2 being Element of F_Complex st z1 in FQ x & z2 in FQ x holds
z1 + z2 in FQ x