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