set F = the strict Field;
reconsider F = the strict Field as comRing ;
reconsider F = F as domRing by VECTSP_2:1;
for x, y being Element of F ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by Lm1;
then F is gcd-like ;
hence ex b₁ being domRing st b₁ is gcd-like ; :: thesis: verum