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