let K be non empty right_complementable associative commutative left_unital Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of K holds <*a*> "*" <*b*> = a * b
let a, b be Element of K; :: thesis: <*a*> "*" <*b*> = a * b
set p = <*a*>;
set q = <*b*>;
set m = mlt (<*a*>,<*b*>);
mlt (<*a*>,<*b*>) = <*(a * b)*> by FINSEQ_2:74;
then mlt (<*a*>,<*b*>) = 1 |-> (a * b) by FINSEQ_2:59;
hence <*a*> "*" <*b*> = a * b by FINSOP_1:16; :: thesis: verum