let h, g be Functional of V; :: thesis: ( ( for v being Vector of V holds h . v = (f . v) *' ) & ( for v being Vector of V holds g . v = (f . v) *' ) implies h = g )
assume that
A2: for a being Vector of V holds h . a = (f . a) *' and
A3: for a being Vector of V holds g . a = (f . a) *' ; :: thesis: h = g

now

let a be Vector of V; :: thesis: h . a = g . a
thus h . a = (f . a) *' by A2
.= g . a by A3 ; :: thesis: verum

end;

hence h = g by FUNCT_2:113; :: thesis: verum