set F = the strict Field;
for x, y being Element of the strict Field ex z being Element of the strict Field st
( z divides x & z divides y & ( for zz being Element of the strict Field st zz divides x & zz divides y holds
zz divides z ) ) by Lm1;
then the strict Field is gcd-like ;
hence ex b₁ being non empty multLoopStr_0 st
( b₁ is gcd-like & b₁ is associative & b₁ is commutative & b₁ is well-unital ) ; :: thesis: verum