let V be non trivial free Z_Module; :: thesis: 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 )
let f be non constant 0-preserving FrFunctional of V; :: thesis: ex v being Vector of V st
( v <> 0. V & f . v <> 0. F_Real )
A1: f . (0. V) = 0. F_Real by HDef9;
assume A2: for v being Vector of V st v <> 0. V holds
f . v = 0. F_Real ; :: thesis: contradiction

now :: thesis: for x, y being object st x in dom f & y in dom f holds
f . x = f . y

let x, y be object ; :: thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume ( x in dom f & y in dom f ) ; :: thesis: f . x = f . y
then reconsider v = x, w = y as Vector of V ;
thus f . x = f . v
.= 0 by A2, A1
.= f . w by A2, A1
.= f . y ; :: thesis: verum

end;

hence contradiction by FUNCT_1:def 10; :: thesis: verum