A1: ( f . (0. V) = 0. K & the carrier of V = dom f ) by FUNCT_2:def 1, HAHNBAN1:def 9;
hereby :: thesis: ( f = 0Functional V implies f is constant )
assume A2: f is constant ; :: thesis: f = 0Functional V
now :: thesis: for v being Vector of V holds f . v = (0Functional V) . v
let v be Vector of V; :: thesis: f . v = (0Functional V) . v
thus f . v = 0. K by A1, A2
.= (0Functional V) . v by HAHNBAN1:14 ; :: thesis: verum
end;
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. K by HAHNBAN1:14
.= (0Functional V) . w by HAHNBAN1:14
.= f . y by A3 ; :: thesis: verum
end;
hence f is constant ; :: thesis: verum