take
F_Complex
; :: thesis: ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated )

thus ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated ) ; :: thesis: verum

thus ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated ) ; :: thesis: verum