let R be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for i being Element of INT.Ring holds (Int-mult-left R) . (i,(0. R)) = 0. R
let i be Element of INT.Ring; :: thesis: (Int-mult-left R) . (i,(0. R)) = 0. R
reconsider ii = i as Element of INT ;
per cases ( 0 <= i or 0 > i ) ;
suppose 0 <= i ; :: thesis: (Int-mult-left R) . (i,(0. R)) = 0. R
then reconsider i1 = i as Element of NAT by INT_1:3;
thus (Int-mult-left R) . (i,(0. R)) = (Nat-mult-left R) . (i1,(0. R)) by Def23
.= 0. R by Th153 ; :: thesis: verum
end;
suppose A1: 0 > i ; :: thesis: (Int-mult-left R) . (i,(0. R)) = 0. R
then reconsider i1 = - ii as Element of NAT by INT_1:3;
thus (Int-mult-left R) . (i,(0. R)) = (Nat-mult-left R) . ((- i),(- (0. R))) by Def23, A1
.= (Nat-mult-left R) . (i1,(0. R)) by RLVECT_1:12
.= 0. R by Th153 ; :: thesis: verum
end;
end;