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 ) )

ex q, r being Element of F st

( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ; :: thesis: verum

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 ) )

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 ) )

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 ) )

( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) ; :: thesis: verum

end;( 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

hence
( b <> 0. F implies ex q, r being Element of F st
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;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

( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) ; :: thesis: verum

ex q, r being Element of F st

( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ; :: thesis: verum