assume A1: A = X ; :: thesis:
assume A2: B = Y ; :: thesis:
( len (A + B) = n & len A = n & width (A + B) = n & width A = n ) by MATRIX_0:24;
then A3: ( len (A + B) = len A & width (A + B) = width A ) ;
A4: ( len X = len A & width X = width A ) by A1;
A5: ( len (X + Y) = len X & width (X + Y) = width X ) by MATRIX_3:def 3;
A6: ( len (X + Y) = len (A + B) & width (X + Y) = width (A + B) ) by A3, A4, A5;
for i, j being Nat st [i,j] in Indices (X + Y) holds
(X + Y) * (i,j) = (A + B) * (i,j)

let i, j be Nat; :: thesis:
assume A7: [i,j] in Indices (X + Y) ; :: thesis:
then [i,j] in [:(dom (X + Y)),(Seg (width (X + Y))):] ;
then ( i in dom (X + Y) & j in Seg (width (X + Y)) ) by ZFMISC_1:87;
then ( 1 <= i & i <= len (X + Y) & 1 <= j & j <= width (X + Y) ) by FINSEQ_1:1, FINSEQ_3:25;
then A8: [i,j] in Indices X by A5, MATRIX_0:30;
then A9: [i,j] in Indices A by A1;
thus (X + Y) * (i,j) = (X * (i,j)) + (Y * (i,j)) by A8, MATRIX_3:def 3
.= (A * (i,j)) + (Y * (i,j)) by A1
.= (A * (i,j)) + (B * (i,j)) by A2
.= (A + B) * (i,j) by A9, MATRIX_1:def 5 ; :: thesis:

end;