let K be non empty right_complementable 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;
hence <*a*> "*" <*b*> = a * b by RLVECT_1:44; :: thesis: verum