let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; :: thesis: F is Euclidian
consider f being Function of the carrier 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 f . r < f . b ) ) by Lm9;
hence F is Euclidian by Def9; :: thesis: verum