let R be non empty addLoopStr ; :: thesis: for a being Element of R
for i being Integer st i = 0 holds
(Int-mult-left R) . (i,a) = 0. R
let a be Element of R; :: thesis: for i being Integer st i = 0 holds
(Int-mult-left R) . (i,a) = 0. R
let i be Integer; :: thesis: ( i = 0 implies (Int-mult-left R) . (i,a) = 0. R )
assume i = 0 ; :: thesis: (Int-mult-left R) . (i,a) = 0. R
hence (Int-mult-left R) . (i,a) = 0 * a by Def23
.= 0. R by BINOM:12 ;
:: thesis: verum