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 Th10;
then the_inverseOp_wrt the addF of K is_distributive_wrt the addF of K by Th17, FINSEQOP:67;
hence comp K is_distributive_wrt the addF of K by Th18; :: thesis: verum