theorem :: ZMODLAT1:54

for V being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds (1. F_Real) * f = f