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

now

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:83, FUNCOP_1:85
.= (NulForm V,W) . v,w by FUNCOP_1:85 ; :: thesis: verum

end;

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