let K be Field; :: thesis: for V being non trivial VectSp of K
for f being constant 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
let V be non trivial VectSp of K; :: thesis: for f being constant 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
let f be constant 0-preserving Functional of V; :: thesis: ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
A1: f . (0. V) = 0. K by HAHNBAN1:def 9;
assume A2: for v being Vector of V st v <> 0. V holds
f . v = 0. K ; :: 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. K by A2, A1
.= f . w by A2, A1
.= f . y ; :: thesis: verum

end;

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