let i be Element of NAT ; :: thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th17, Th18;
hence Sum (R1 - R2) = (diffield K) . ((Sum R1),( the addF of K $$ R2)) by Th10, SETWOP_2:48
.= (Sum R1) - (Sum R2) by Th14 ;
:: thesis: verum