let V be non trivial free Z_Module; :: thesis: for f being V8() 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. INT.Ring )
let f be V8() 0-preserving Functional of V; :: thesis: ex v being Vector of V st
( v <> 0. V & f . v <> 0. INT.Ring )
A1: f . (0. V) = 0. INT.Ring by HAHNBAN1:def 9;
assume A2: for v being Vector of V st v <> 0. V holds
f . v = 0. INT.Ring ; :: 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