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