let seq1, seq be Complex_Sequence; :: thesis: for Ns being V36() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
let Ns be V36() sequence of NAT ; :: thesis: (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
thus (seq1 /" seq) * Ns = (seq1 * Ns) (#) ((seq " ) * Ns) by Th9
.= (seq1 * Ns) /" (seq * Ns) by Th12 ; :: thesis: verum