let K be Field; :: thesis: for V being non trivial VectSp of K

for f being V8() 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 V8() 0-preserving Functional of V ex v being Vector of V st

( v <> 0. V & f . v <> 0. K )

let f be V8() 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

for f being V8() 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 V8() 0-preserving Functional of V ex v being Vector of V st

( v <> 0. V & f . v <> 0. K )

let f be V8() 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

hence
contradiction
by FUNCT_1:def 10; :: thesis: verumf . 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;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