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