let u be VECTOR of ((0). V); :: thesis: for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
let a be Real; :: thesis: niltonil . (a * u) = (abs a) * (niltonil . u)
niltonil . u = 0 by FUNCOP_1:13;
hence niltonil . (a * u) = (abs a) * (niltonil . u) by FUNCOP_1:13; :: thesis: verum