ex z being Element of R st x = y * z by A1, Def1;
hence ex b₁ being Element of R st b₁ * y = x ; :: thesis: verum