let K be non empty multMagma ; :: thesis: for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
let a1, a2, b1, b2 be Element of K; :: thesis: mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
( <*a1,a2*> = <*a1*> ^ <*a2*> & <*b1,b2*> = <*b1*> ^ <*b2*> ) by FINSEQ_1:def 9;
hence mlt (<*a1,a2*>,<*b1,b2*>) = (mlt (<*a1*>,<*b1*>)) ^ <*(a2 * b2)*> by FINSEQOP:10
.= <*(a1 * b1)*> ^ <*(a2 * b2)*> by FINSEQ_2:74
.= <*(a1 * b1),(a2 * b2)*> by FINSEQ_1:def 9 ;
:: thesis: verum