let n be Nat; :: thesis: for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (- A) = 0. (F,n)

let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of n,F holds A + (- A) = 0. (F,n)
let A be Matrix of n,F; :: thesis: A + (- A) = 0. (F,n)
A1: Indices A = Indices (A + (- A)) by MATRIX_0:26;
A2: Indices A = Indices (0. (F,n)) by MATRIX_0:26;
now :: thesis: for i, j being Nat st [i,j] in Indices (A + (- A)) holds
(A + (- A)) * (i,j) = (0. (F,n)) * (i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices (A + (- A)) implies (A + (- A)) * (i,j) = (0. (F,n)) * (i,j) )
assume A3: [i,j] in Indices (A + (- A)) ; :: thesis: (A + (- A)) * (i,j) = (0. (F,n)) * (i,j)
hence (A + (- A)) * (i,j) = (A * (i,j)) + ((- A) * (i,j)) by
.= (A * (i,j)) + (- (A * (i,j))) by A1, A3, Def4
.= 0. F by RLVECT_1:def 10
.= (0. (F,n)) * (i,j) by A2, A1, A3, Th1 ;
:: thesis: verum
end;
hence A + (- A) = 0. (F,n) by MATRIX_0:27; :: thesis: verum