let u, v be VECTOR of ((0). V0); :: thesis: for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
let a be Real; :: thesis: nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
( u = 0. V0 & v = 0. V0 ) by Lm1, TARSKI:def 1;
hence nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) by Lm1, Lm2, TARSKI:def 1; :: thesis: verum