let u, v be VECTOR of ((0). the ComplexLinearSpace); :: thesis: for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
let a be Complex; :: thesis: nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
A1: v = 0. the ComplexLinearSpace by Lm2, TARSKI:def 1;
u = 0. the ComplexLinearSpace by Lm2, TARSKI:def 1;
hence nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) by A1, Lm2, Lm4, TARSKI:def 1; :: thesis: verum