thus for v being Vector of (DivisibleMod V) holds v is divisible by ThDivisible1; :: according to ZMODUL08:def 2 :: thesis: verum