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 ) ;
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