let i be Nat; :: thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
let R be Element of i -tuples_on the carrier of K; :: thesis: R + (- R) = i |-> (0. K)
A1: ( the addF of K is having_an_inverseOp & the addF of K is having_a_unity ) by Th8, Th14;
thus R + (- R) = the addF of K .: (R,((the_inverseOp_wrt the addF of K) * R)) by Th15
.= i |-> (the_unity_wrt the addF of K) by A1, FINSEQOP:73
.= i |-> (0. K) by Th7 ; :: thesis: verum