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