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