theorem Lm52: :: ALGNUM_1:42

for x being Element of F_Complex holds In ((1. F_Complex),(FQ x)) = 1. F_Complex