let u, v be VECTOR of ((0). the ComplexLinearSpace); :: thesis: niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
( u = 0. the ComplexLinearSpace & v = 0. the ComplexLinearSpace ) by Lm7, TARSKI:def 1;
hence niltonil . (u + v) <= (niltonil . u) + (niltonil . v) by Lm7, Lm8, TARSKI:def 1; :: thesis: verum