let K be non empty right_complementable associative left_unital Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
let a1, a2, b1, b2 be Element of K; :: thesis: <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
set p = <*a1,a2*>;
set q = <*b1,b2*>;
the addF of K $$ (mlt (<*a1,a2*>,<*b1,b2*>)) = the addF of K $$ <*(a1 * b1),(a2 * b2)*> by Lm5
.= (a1 * b1) + (a2 * b2) by FINSOP_1:12 ;
hence <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) ; :: thesis: verum