set F = the strict Field;
take the strict Field ; :: thesis: ( the strict Field is strict & the strict Field is Abelian & the strict Field is add-associative & the strict Field is right_zeroed & the strict Field is right_complementable & the strict Field is associative & the strict Field is commutative & the strict Field is distributive & the strict Field is unital & the strict Field is domRing-like & the strict Field is almost_left_invertible & not the strict Field is degenerated )
thus ( the strict Field is strict & the strict Field is Abelian & the strict Field is add-associative & the strict Field is right_zeroed & the strict Field is right_complementable & the strict Field is associative & the strict Field is commutative & the strict Field is distributive & the strict Field is unital & the strict Field is domRing-like & the strict Field is almost_left_invertible & not the strict Field is degenerated ) ; :: thesis: verum