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