let seq, seq' be Complex_Sequence; :: thesis: |.(seq (#) seq').| = |.seq.| (#) |.seq'.|

now

let n be Element of NAT ; :: thesis: |.(seq (#) seq').| . n = (|.seq.| (#) |.seq'.|) . n
thus |.(seq (#) seq').| . n = |.((seq (#) seq') . n).| by VALUED_1:18
.= |.((seq . n) * (seq' . n)).| by VALUED_1:5
.= |.(seq . n).| * |.(seq' . n).| by COMPLEX1:151
.= (|.seq.| . n) * |.(seq' . n).| by VALUED_1:18
.= (|.seq.| . n) * (|.seq'.| . n) by VALUED_1:18
.= (|.seq.| (#) |.seq'.|) . n by VALUED_1:5 ; :: thesis: verum

end;

hence |.(seq (#) seq').| = |.seq.| (#) |.seq'.| by FUNCT_2:113; :: thesis: verum