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