let r be Complex; :: thesis: for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|
let seq be Complex_Sequence; :: thesis: |.(r (#) seq).| = |.r.| (#) |.seq.|

now :: thesis: for n being Element of NAT holds |.(r (#) seq).| . n = (|.r.| (#) |.seq.|) . n

let n be Element of NAT ; :: thesis: |.(r (#) seq).| . n = (|.r.| (#) |.seq.|) . n
thus |.(r (#) seq).| . n = |.((r (#) seq) . n).| by VALUED_1:18
.= |.(r * (seq . n)).| by VALUED_1:6
.= |.r.| * |.(seq . n).| by COMPLEX1:65
.= |.r.| * (|.seq.| . n) by VALUED_1:18
.= (|.r.| (#) |.seq.|) . n by VALUED_1:6 ; :: thesis: verum

end;

hence |.(r (#) seq).| = |.r.| (#) |.seq.| by FUNCT_2:63; :: thesis: verum