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

now

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

end;

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