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