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