let K be Ring; :: thesis: for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
let A, B be Matrix of K; :: thesis: ( len A = len B & width A = width B implies A + B = B + A )
assume that
A1: len A = len B and
A2: width A = width B ; :: thesis: A + B = B + A
A3: width A = width (A + B) by Def3;
then A4: width (A + B) = width (B + A) by A2, Def3;
A5: len A = len (A + B) by Def3;
then dom A = dom (A + B) by FINSEQ_3:29;
then A6: Indices A = Indices (A + B) by A3;
dom A = dom B by A1, FINSEQ_3:29;
then A7: Indices B = [:(dom A),(Seg (width A)):] by A2;

A8: now :: thesis: for i, j being Nat st [i,j] in Indices (A + B) holds
(A + B) * (i,j) = (B + A) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices (A + B) implies (A + B) * (i,j) = (B + A) * (i,j) )
assume A9: [i,j] in Indices (A + B) ; :: thesis: (A + B) * (i,j) = (B + A) * (i,j)
hence (A + B) * (i,j) = (B * (i,j)) + (A * (i,j)) by A6, Def3
.= (B + A) * (i,j) by A7, A6, A9, Def3 ;
:: thesis: verum

end;

len (A + B) = len (B + A) by A1, A5, Def3;
hence A + B = B + A by A4, A8, MATRIX_0:21; :: thesis: verum