let K be non empty right_complementable left_unital associative commutative Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a1, a2, a3, b1, b2, b3 being Element of K holds <*a1,a2,a3*> "*" <*b1,b2,b3*> = ((a1 * b1) + (a2 * b2)) + (a3 * b3)
let a1, a2, a3, b1, b2, b3 be Element of K; :: thesis: <*a1,a2,a3*> "*" <*b1,b2,b3*> = ((a1 * b1) + (a2 * b2)) + (a3 * b3)
set p = <*a1,a2,a3*>;
set q = <*b1,b2,b3*>;
Sum (mlt (<*a1,a2,a3*>,<*b1,b2,b3*>)) = the addF of K $$ (mlt (<*a1,a2,a3*>,<*b1,b2,b3*>)) by FVSUM_1:def 8
.= the addF of K $$ <*(a1 * b1),(a2 * b2),(a3 * b3)*> by Th5
.= ((a1 * b1) + (a2 * b2)) + (a3 * b3) by FINSOP_1:14 ;
hence <*a1,a2,a3*> "*" <*b1,b2,b3*> = ((a1 * b1) + (a2 * b2)) + (a3 * b3) by FVSUM_1:def 9; :: thesis: verum