let n be Nat; :: thesis: for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B being Matrix of n,F holds A + B = B + A
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for A, B being Matrix of n,F holds A + B = B + A
let A, B be Matrix of n,F; :: thesis: A + B = B + A
A1: ( Indices A = Indices B & Indices A = Indices (A + B) ) by Th27;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (A + B) implies (A + B) * i,j = (B + A) * i,j )
assume A2: [i,j] in Indices (A + B) ; :: thesis: (A + B) * i,j = (B + A) * i,j
hence (A + B) * i,j = (A * i,j) + (B * i,j) by A1, Def14
.= (B + A) * i,j by A1, A2, Def14 ;
:: thesis: verum

end;

hence A + B = B + A by Th28; :: thesis: verum