thus for x being Vector of ((0). V) holds x is divisible :: according to ZMODUL08:def 2 :: thesis: verum

proof

let x be Vector of ((0). V); :: thesis: x is divisible
x in (0). V ;
then x = 0. V by ZMODUL02:66
.= 0. ((0). V) by ZMODUL01:26 ;
hence x is divisible ; :: thesis: verum

end;