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

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

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

end;

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