for V being non trivial free Z_Module
for f being non constant 0-preserving FrFunctional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. F_Real )