let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; :: thesis: for f being 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 f . r < f . b ) )
let f be Function of F,NAT; :: thesis: 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 ) )

now :: thesis: for a, b being Element of F st b <> 0. F & b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )

let a, b be Element of F; :: thesis: ( b <> 0. F & b <> 0. F implies ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) )
assume A1: b <> 0. F ; :: thesis: ( b <> 0. F implies ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) )
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )

proof

consider x being Element of F such that
A2: x * b = 1. F by A1, VECTSP_1:def 9;
((a * x) * b) + (0. F) = (a * (1. F)) + (0. F) by A2, GROUP_1:def 3
.= a + (0. F)
.= a by RLVECT_1:def 4 ;
hence ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ; :: thesis: verum

end;

hence ( b <> 0. F implies ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) ; :: thesis: verum

end;

hence 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 ) ) ; :: thesis: verum