thus not for v being non zero Vector of V holds v is divisible :: thesis:

proof

assume AS: for v being non zero Vector of V holds v is divisible ; :: thesis:
for v being Vector of V holds v is divisible

proof

let v be Vector of V; :: thesis:

per cases ;

suppose v = 0. V ; :: thesis:

hence v is divisible ; :: thesis:

end;

suppose v <> 0. V ; :: thesis:

then not v is zero ;
hence v is divisible by AS; :: thesis:

end;

end;

end;

hence contradiction by defDivisibleModule; :: thesis:

end;