let u be VECTOR of ((0). the RealLinearSpace); :: thesis: for a being Real holds niltonil . (a * u) = |.a.| * (niltonil . u)
let a be Real; :: thesis: niltonil . (a * u) = |.a.| * (niltonil . u)
niltonil . u = 0 by FUNCOP_1:7;
hence niltonil . (a * u) = |.a.| * (niltonil . u) by FUNCOP_1:7; :: thesis: verum