let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; :: thesis: for f being Function of F,NAT holds f is DegreeFunction of F

let f be Function of F,NAT; :: thesis: f is DegreeFunction of F

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 Lm4;

hence f is DegreeFunction of F by Def9; :: thesis: verum

let f be Function of F,NAT; :: thesis: f is DegreeFunction of F

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 Lm4;

hence f is DegreeFunction of F by Def9; :: thesis: verum