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