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 - (i |-> (0. K)) = R
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 - (i |-> (0. K)) = R
let R be Element of i -tuples_on the carrier of K; :: thesis: R - (i |-> (0. K)) = R
thus R - (i |-> (0. K)) = R + (- (i |-> (0. K))) by FINSEQOP:84
.= R + (i |-> (- (0. K))) by Th25
.= R + (i |-> (0. K)) by RLVECT_1:12
.= R by Lm2 ; :: thesis: verum