let a, b be Element of INT.Ring; :: thesis: ( b <> 0. INT.Ring implies a = ((a div b) * b) + (a mod b) )
consider d being Element of INT.Ring such that
A1: d = a div b ;
assume A2: b <> 0. INT.Ring ; :: thesis: a = ((a div b) * b) + (a mod b)
then ex r being Element of INT.Ring st
( a = (d * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Def7;
hence a = ((a div b) * b) + (a mod b) by A2, A1, Def8; :: thesis: verum