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:11
.= <*(a1 * b1)*> ^ <*(a2 * b2)*> by FINSEQ_2:88
.= <*(a1 * b1),(a2 * b2)*> by FINSEQ_1:def 9 ;
:: thesis: verum