take N_Real ; :: thesis:
thus ( N_Real is strict & not N_Real is degenerated & N_Real is real-membered & N_Real is reflexive & N_Real is discerning & N_Real is zeroed & N_Real is complementable & N_Real is add-associative & N_Real is Abelian & N_Real is associative & N_Real is commutative & N_Real is distributive & N_Real is well-unital & N_Real is add-cancelable & N_Real is vector-associative & N_Real is vector-distributive & N_Real is scalar-distributive & N_Real is scalar-associative & N_Real is scalar-unital & N_Real is Banach_Algebra-like_1 & N_Real is Banach_Algebra-like_2 & N_Real is Banach_Algebra-like_3 & N_Real is well-conjugated & N_Real is add-conjugative & N_Real is norm-conjugative & N_Real is scalar-conjugative & N_Real is almost_left_invertible & N_Real is almost_left_cancelable & N_Real is RealNormSpace-like ) ; :: thesis: