let seq, seq1 be Complex_Sequence; :: thesis: (seq ") (#) (seq1 ") = (seq (#) seq1) "

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

let n be Element of NAT ; :: thesis: ((seq ") (#) (seq1 ")) . n = ((seq (#) seq1) ") . n
thus ((seq ") (#) (seq1 ")) . n = ((seq ") . n) * ((seq1 ") . n) by VALUED_1:5
.= ((seq ") . n) * ((seq1 . n) ") by VALUED_1:10
.= ((seq . n) ") * ((seq1 . n) ") by VALUED_1:10
.= ((seq . n) * (seq1 . n)) " by XCMPLX_1:204
.= ((seq (#) seq1) . n) " by VALUED_1:5
.= ((seq (#) seq1) ") . n by VALUED_1:10 ; :: thesis: verum

end;

hence (seq ") (#) (seq1 ") = (seq (#) seq1) " by FUNCT_2:63; :: thesis: verum