let K be Field; :: thesis: for A, B, C being Matrix of K st len A = len B & width A = width B holds
(A + B) + C = A + (B + C)
let A, B, C be Matrix of K; :: thesis: ( len A = len B & width A = width B implies (A + B) + C = A + (B + C) )
assume that
A1: len A = len B and
A2: width A = width B ; :: thesis: (A + B) + C = A + (B + C)
dom A = dom B by A1, FINSEQ_3:31;
then A3: Indices B = [:(dom A),(Seg (width A)):] by A2, MATRIX_1:def 5;
A4: Indices A = [:(dom A),(Seg (width A)):] by MATRIX_1:def 5;
A5: width ((A + B) + C) = width (A + B) by Def3;
A6: width (A + B) = width A by Def3;
A7: ( len (A + (B + C)) = len A & width (A + (B + C)) = width A ) by Def3;
A8: len (A + B) = len A by Def3;
A9: len ((A + B) + C) = len (A + B) by Def3;
then dom A = dom ((A + B) + C) by A8, FINSEQ_3:31;
then A10: Indices ((A + B) + C) = [:(dom A),(Seg (width A)):] by A6, A5, MATRIX_1:def 5;
dom A = dom (A + B) by A8, FINSEQ_3:31;
then A11: Indices (A + B) = [:(dom A),(Seg (width A)):] by A6, MATRIX_1:def 5;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((A + B) + C) implies ((A + B) + C) * i,j = (A + (B + C)) * i,j )
assume A12: [i,j] in Indices ((A + B) + C) ; :: thesis: ((A + B) + C) * i,j = (A + (B + C)) * i,j
hence ((A + B) + C) * i,j = ((A + B) * i,j) + (C * i,j) by A11, A10, Def3
.= ((A * i,j) + (B * i,j)) + (C * i,j) by A4, A10, A12, Def3
.= (A * i,j) + ((B * i,j) + (C * i,j)) by RLVECT_1:def 6
.= (A * i,j) + ((B + C) * i,j) by A3, A10, A12, Def3
.= (A + (B + C)) * i,j by A4, A10, A12, Def3 ;
:: thesis: verum

end;

hence (A + B) + C = A + (B + C) by A8, A6, A9, A5, A7, MATRIX_1:21; :: thesis: verum