let V, W be non empty ModuleStr over F_Complex ; :: thesis: (NulForm (V,W)) *' = NulForm (V,W)
set f = NulForm (V,W);

now :: thesis: for v being Vector of V
for w being Vector of W holds ((NulForm (V,W)) *') . (v,w) = (NulForm (V,W)) . (v,w)

let v be Vector of V; :: thesis: for w being Vector of W holds ((NulForm (V,W)) *') . (v,w) = (NulForm (V,W)) . (v,w)
let w be Vector of W; :: thesis: ((NulForm (V,W)) *') . (v,w) = (NulForm (V,W)) . (v,w)
thus ((NulForm (V,W)) *') . (v,w) = ((NulForm (V,W)) . (v,w)) *' by Def8
.= 0. F_Complex by COMPLFLD:47, FUNCOP_1:70
.= (NulForm (V,W)) . (v,w) by FUNCOP_1:70 ; :: thesis: verum

end;

hence (NulForm (V,W)) *' = NulForm (V,W) ; :: thesis: verum