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

set f = 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)

hence
(NulForm (V,W)) *' = NulForm (V,W)
; :: thesis: verumfor 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;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