:: deftheorem defines indeterminate RING_EMB:def 12 :
for R being non degenerated comRing
for A being b₁ -monomorphic comRing
for x being Element of A holds
( x is indeterminate iff ex g being Function of (Polynom-Ring R),A st
( g is isomorphism & x = g . (1_1 R) ) );