let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: comp K is_distributive_wrt the addF of K
the addF of K is having_a_unity by Th8;
then the_inverseOp_wrt the addF of K is_distributive_wrt the addF of K by Th14, FINSEQOP:63;
hence comp K is_distributive_wrt the addF of K by Th15; :: thesis: verum