theorem Lm47: :: ALGNUM_1:38

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