let i be Nat; :: thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R
let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R
let R be Element of i -tuples_on the carrier of K; :: thesis: (i |-> (0. K)) - R = - R
thus (i |-> (0. K)) - R = (i |-> (0. K)) + (- R) by FINSEQOP:84
.= - R by Th21 ; :: thesis: verum