:: deftheorem defines NulForm ZMATRLIN:def 12 :
for V, W being ModuleStr over INT.Ring holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. INT.Ring);