let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; :: thesis: F is Euclidian
set f = the Function of F,NAT;
for a, b being Element of F st b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or the Function of F,NAT . r < the Function of F,NAT . b ) ) by Lm4;
hence F is Euclidian ; :: thesis: verum