theorem :: ZMODUL01:110

for V being strict Z_Module holds ((Omega). V) /\ ((Omega). V) = V by Th109;