A1: f . (0. V) = 0. K by HAHNBAN1:def 13;
A2: the carrier of V = dom f by FUNCT_2:def 1;

hereby :: thesis: ( f = 0Functional V implies f is constant )

assume A3: f is constant ; :: thesis: f = 0Functional V

now

let v be Vector of V; :: thesis: f . v = (0Functional V) . v
thus f . v = 0. K by A1, A2, A3, FUNCT_1:def 16
.= (0Functional V) . v by HAHNBAN1:22 ; :: thesis: verum

end;

hence f = 0Functional V by FUNCT_2:113; :: thesis: verum

end;

assume A4: f = 0Functional V ; :: thesis: f is constant

now

let x, y be set ; :: thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume A5: ( x in dom f & y in dom f ) ; :: thesis: f . x = f . y
reconsider v = x, w = y as Vector of V by A5;
thus f . x = (0Functional V) . v by A4
.= 0. K by HAHNBAN1:22
.= (0Functional V) . w by HAHNBAN1:22
.= f . y by A4 ; :: thesis: verum

end;

hence f is constant by FUNCT_1:def 16; :: thesis: verum