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

proof

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

proof

let v be Vector of V; :: thesis: v is divisible

per cases ( v = 0. V or v <> 0. V ) ;

suppose v = 0. V ; :: thesis: v is divisible

hence v is divisible ; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction by defDivisibleModule; :: thesis: verum

end;