let u be VECTOR of ((0). the ComplexLinearSpace); :: 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:7;
hence niltonil . (z * u) = |.z.| * (niltonil . u) by FUNCOP_1:7; :: thesis: verum