let A be non degenerated commutative Ring; :: thesis: 0. A is Zero_Divisor of A
consider b being Element of A such that
A1: b = 1. A ;
(0. A) * b = 0. A ;
then 0. A is zero_divisible by A1;
hence 0. A is Zero_Divisor of A ; :: thesis: verum