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