let a, b be FrFunctional of V; :: thesis: ( ( for x being Element of V holds a . x = v * (f . x) ) & ( for x being Element of V holds b . x = v * (f . x) ) implies a = b )
assume that
A2: for x being Element of V holds a . x = v * (f . x) and
A3: for x being Element of V holds b . x = v * (f . x) ; :: thesis: a = b

now :: thesis: for x being Element of V holds a . x = b . x

let x be Element of V; :: thesis: a . x = b . x
thus a . x = v * (f . x) by A2
.= b . x by A3 ; :: thesis: verum

end;

hence a = b by FUNCT_2:63; :: thesis: verum