theorem :: ALGNUM_1:55

for x being Element of F_Complex st x is algebraic holds
FQ_Ring x is Field