let V be Z_Module; :: thesis: for a being Element of INT.Ring
for v being Vector of V st ( a = 0. INT.Ring or v = 0. V ) holds
a * v = 0. V
let a be Element of INT.Ring; :: thesis: for v being Vector of V st ( a = 0. INT.Ring or v = 0. V ) holds
a * v = 0. V
let v be Vector of V; :: thesis: ( ( a = 0. INT.Ring or v = 0. V ) implies a * v = 0. V )
set R = INT.Ring ;
set N1 = 1. INT.Ring;
set N0 = 0. INT.Ring;
assume A1: ( a = 0. INT.Ring or v = 0. V ) ; :: thesis: a * v = 0. V
now :: thesis: a * v = 0. V
per cases ( a = 0. INT.Ring or v = 0. V ) by A1;
suppose A2: a = 0. INT.Ring ; :: thesis: a * v = 0. V
v + ((0. INT.Ring) * v) = ((1. INT.Ring) * v) + ((0. INT.Ring) * v) by VECTSP_1:def 17
.= ((1. INT.Ring) + (0. INT.Ring)) * v by VECTSP_1:def 15
.= v by VECTSP_1:def 17
.= v + (0. V) by RLVECT_1:4 ;
hence a * v = 0. V by A2, RLVECT_1:8; :: thesis: verum
end;
suppose A3: v = 0. V ; :: thesis: a * v = 0. V
(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by VECTSP_1:def 14
.= a * (0. V) by RLVECT_1:4
.= (a * (0. V)) + (0. V) by RLVECT_1:4 ;
hence a * v = 0. V by A3, RLVECT_1:8; :: thesis: verum
end;
end;
end;
hence a * v = 0. V ; :: thesis: verum