for R being Ring
for x being Vector of (TrivialLMod R) holds x = 0. (TrivialLMod R) by GRCAT_1:4;