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

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