let u, v, w be VECTOR of ((0). the ComplexLinearSpace); 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; verum