let V be non empty VectSpStr of F_Complex ; :: thesis: for f being Functional of V holds (f *' ) *' = f
let f be Functional of V; :: thesis: (f *' ) *' = f

now

let v be Vector of V; :: thesis: ((f *' ) *' ) . v = f . v
thus ((f *' ) *' ) . v = ((f *' ) . v) *' by Def2
.= ((f . v) *' ) *' by Def2
.= f . v ; :: thesis: verum

end;

hence (f *' ) *' = f by FUNCT_2:113; :: thesis: verum