theorem :: INT_3:6

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