let u, v be VECTOR of ((0). the ComplexLinearSpace); :: thesis: nilfunc . [u,v] = (nilfunc . [v,u]) *'
A1: v = 0. the ComplexLinearSpace by Lm2, TARSKI:def 1;
u = 0. the ComplexLinearSpace by Lm2, TARSKI:def 1;
hence nilfunc . [u,v] = (nilfunc . [v,u]) *' by A1, Lm4, COMPLEX1:28; :: thesis: verum