let K be non empty right_complementable associative commutative left_unital Abelian add-associative right_zeroed doubleLoopStr ; 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; <*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)
; verum