let u, v be VECTOR of ((0). V0); :: thesis: nilfunc . [u,v] = (nilfunc . [v,u]) *'
( u = 0. V0 & v = 0. V0 ) by Lm1, TARSKI:def 1;
hence nilfunc . [u,v] = (nilfunc . [v,u]) *' by Lm3, COMPLEX1:113; :: thesis: verum