let K be Ring; :: 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:29;
then A3: Indices B = [:(dom A),(Seg (width A)):] by A2;
A4: Indices A = [:(dom A),(Seg (width A)):] ;
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:29;
then A10: Indices ((A + B) + C) = [:(dom A),(Seg (width A)):] by A6, A5;
dom A = dom (A + B) by A8, FINSEQ_3:29;
then A11: Indices (A + B) = [:(dom A),(Seg (width A)):] by A6;

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

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 3
.= (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_0:21; :: thesis: verum