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 almost_left_invertible & 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 almost_left_invertible & not F_Complex is degenerated ) ; :: thesis: verum