let A be non degenerated commutative Ring; :: thesis: ( A is domRing implies {(0. A)} = ZeroDiv_Set A )
assume A0: A is domRing ; :: thesis: {(0. A)} = ZeroDiv_Set A
0. A is Zero_Divisor of A by Th1;
then A1: 0. A in ZeroDiv_Set A ;
A2: {(0. A)} is Subset of (ZeroDiv_Set A) by A1, SUBSET_1:33;
for o being object st o in ZeroDiv_Set A holds
o in {(0. A)}
proof
let o be object ; :: thesis: ( o in ZeroDiv_Set A implies o in {(0. A)} )
assume o in ZeroDiv_Set A ; :: thesis: o in {(0. A)}
then consider a being Element of [#] A such that
A4: o = a and
A5: a is Zero_Divisor of A ;
consider b being Element of A such that
A6: b <> 0. A and
A7: a * b = 0. A by A5, Def1;
a = 0. A by A6, A0, A7, VECTSP_2:def 1;
hence o in {(0. A)} by A4, TARSKI:def 1; :: thesis: verum
end;
then ZeroDiv_Set A c= {(0. A)} ;
hence {(0. A)} = ZeroDiv_Set A by A2, XBOOLE_0:def 10; :: thesis: verum