let K be non empty multMagma ; :: thesis: for a1, a2, a3, b1, b2, b3 being Element of K holds mlt (<*a1,a2,a3*>,<*b1,b2,b3*>) = <*(a1 * b1),(a2 * b2),(a3 * b3)*>
let a1, a2, a3, b1, b2, b3 be Element of K; :: thesis: mlt (<*a1,a2,a3*>,<*b1,b2,b3*>) = <*(a1 * b1),(a2 * b2),(a3 * b3)*>
thus mlt (<*a1,a2,a3*>,<*b1,b2,b3*>) = the multF of K .: (<*a1,a2,a3*>,<*b1,b2,b3*>) by FVSUM_1:def 7
.= <*(a1 * b1),(a2 * b2),(a3 * b3)*> by FINSEQ_2:76 ; :: thesis: verum