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 + (0. F,n) = A
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of n,F holds A + (0. F,n) = A
let A be Matrix of n,F; :: thesis: A + (0. F,n) = A
A1: Indices A = Indices (A + (0. F,n)) by Th27;
A2: Indices A = Indices (0. F,n) by Th27;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (A + (0. F,n)) implies (A + (0. F,n)) * i,j = A * i,j )
assume A3: [i,j] in Indices (A + (0. F,n)) ; :: thesis: (A + (0. F,n)) * i,j = A * i,j
hence (A + (0. F,n)) * i,j = (A * i,j) + ((0. F,n) * i,j) by A1, Def14
.= (A * i,j) + (0. F) by A1, A2, A3, Th30
.= A * i,j by RLVECT_1:10 ;
:: thesis: verum

end;

hence A + (0. F,n) = A by Th28; :: thesis: verum