theorem ThTrivial1: :: ZMODUL07:41

for V being trivial Z_Module holds (Omega). V = (0). V