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