let V be non empty ModuleStr over F_Complex ; :: thesis: (0Functional V) *' = 0Functional V
set f = 0Functional V;

now :: thesis: for v being Vector of V holds ((0Functional V) *') . v = (0Functional V) . v

let v be Vector of V; :: thesis: ((0Functional V) *') . v = (0Functional V) . v
thus ((0Functional V) *') . v = ((0Functional V) . v) *' by Def2
.= 0. F_Complex by COMPLFLD:47, HAHNBAN1:14
.= (0Functional V) . v by HAHNBAN1:14 ; :: thesis: verum

end;

hence (0Functional V) *' = 0Functional V by FUNCT_2:63; :: thesis: verum