for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds
ex b being Element of F_Complex st
( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex )