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 ex b₁ being Element of A st b₁ is zero_divisible ; :: thesis: verum