let f be Functional of V; :: thesis: ( not f is degenerated & f is 0-preserving implies not f is constant )
assume that
A1: not f is degenerated and
A2: f is 0-preserving and
A3: f is constant ; :: thesis: contradiction
A4: f . (0. V) = 0. K by A2;

A5: now :: thesis: ex v being Vector of V st
( v <> 0. V & not f . v = 0. K )

assume A6: for v being Vector of V st v <> 0. V holds
f . v = 0. K ; :: thesis: contradiction
the carrier of V c= ker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of V or x in ker f )
assume x in the carrier of V ; :: thesis: x in ker f
then reconsider v = x as Vector of V ;

per cases ( v = 0. V or v <> 0. V ) ;

suppose v = 0. V ; :: thesis: x in ker f

hence x in ker f by A4; :: thesis: verum

end;

suppose v <> 0. V ; :: thesis: x in ker f

then f . v = 0. K by A6;
hence x in ker f ; :: thesis: verum

end;

end;

end;

then the carrier of V = ker f
.= {(0. V)} by A1 ;
hence contradiction ; :: thesis: verum

end;

dom f = the carrier of V by FUNCT_2:def 1;
hence contradiction by A3, A4, A5; :: thesis: verum