A1: ( f . (0. V) = 0. INT.Ring & the carrier of V = dom f ) by FUNCT_2:def 1, HAHNBAN1:def 9;

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

assume f is constant ; :: thesis: f = 0Functional V
then for v being Vector of V holds f . v = (0Functional V) . v by A1;
hence f = 0Functional V by FUNCT_2:63; :: thesis: verum

end;

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

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 = (0Functional V) . v by A3
.= 0
.= (0Functional V) . w
.= f . y by A3 ; :: thesis: verum

end;

hence f is constant ; :: thesis: verum