theorem :: ZMATRLIN:66

for V, W being non empty ModuleStr over INT.Ring
for f being Form of V,W holds (1. INT.Ring) * f = f