let K be non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital 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:88;
then mlt (<*a*>,<*b*>) = 1 |-> (a * b) by FINSEQ_2:73;
hence <*a*> "*" <*b*> = a * b by FINSOP_1:17; :: thesis: verum