let K be Field; :: 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: Indices A = [:(dom A),(Seg (width A)):] by MATRIX_1:def 5;
A6: len A = len (A + B) by Def3;
then dom A = dom (A + B) by FINSEQ_3:31;
then A7: Indices A = Indices (A + B) by A5, A3, MATRIX_1:def 5;
dom A = dom B by A1, FINSEQ_3:31;
then A8: Indices B = [:(dom A),(Seg (width A)):] by A2, MATRIX_1:def 5;

A9: now

let i, j be Nat; :: thesis: ( [i,j] in Indices (A + B) implies (A + B) * i,j = (B + A) * i,j )
assume A10: [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 A7, Def3
.= (B + A) * i,j by A5, A8, A7, A10, Def3 ;
:: thesis: verum

end;

len (A + B) = len (B + A) by A1, A6, Def3;
hence A + B = B + A by A4, A9, MATRIX_1:21; :: thesis: verum