let a be Integer; :: thesis: for V being Z_Module
for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let V be Z_Module; :: thesis: for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let v be VECTOR of V; :: thesis: ( ( a = 0 or v = 0. V ) implies a * v = 0. V )
reconsider N1 = 1, N0 = 0 as Integer ;
assume A1: ( a = 0 or v = 0. V ) ; :: thesis: a * v = 0. V

now :: thesis: a * v = 0. V

per cases ( a = 0 or v = 0. V ) by A1;

suppose A2: a = 0 ; :: thesis: a * v = 0. V

v + (N0 * v) = (N1 * v) + (N0 * v) by Def5
.= (N1 + N0) * v by Def3
.= v by Def5
.= 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 Def2
.= 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