let u, v be VECTOR of ((0). the RealLinearSpace); :: thesis: nilfunc . [u,v] = nilfunc . [v,u]
( u = 0. the RealLinearSpace & v = 0. the RealLinearSpace ) by Lm1, TARSKI:def 1;
hence nilfunc . [u,v] = nilfunc . [v,u] ; :: thesis: verum