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

set f = 0Functional V;

set f = 0Functional V;

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

hence
(0Functional V) *' = 0Functional V
by FUNCT_2:63; :: thesis: verumlet 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;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