:: deftheorem Def3 defines Psi IDEAL_2:def 3 :
for A being non degenerated commutative Ring
for q being Ideal of A
for b₃ being Function of (Ideals (A / q)),(Ideals (A,q)) holds
( b₃ = Psi q iff for x being Element of Ideals (A / q) holds b₃ . x = (canHom q) " x );