let R be Ring; :: thesis: for n being Nat
for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a + b = A + B
let n be Nat; :: thesis: for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a + b = A + B
let S be Subring of R; :: thesis: for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a + b = A + B
let a, b be Matrix of n,S; :: thesis: for A, B being Matrix of n,R st a = A & b = B holds
a + b = A + B
let A, B be Matrix of n,R; :: thesis: ( a = A & b = B implies a + b = A + B )
assume A1: a = A ; :: thesis: ( not b = B or a + b = A + B )
assume A2: b = B ; :: thesis: a + b = A + B
set LHS = a + b;
set RHS = A + B;
for i, j being Nat st [i,j] in Indices (a + b) holds
(a + b) * (i,j) = (A + B) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a + b) implies (a + b) * (i,j) = (A + B) * (i,j) )
assume A3: [i,j] in Indices (a + b) ; :: thesis: (a + b) * (i,j) = (A + B) * (i,j)
A4: Indices a = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (a + b) by MATRIX_0:24 ;
A5: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (a + b) by MATRIX_0:24 ;
A6: (A * (i,j)) + (B * (i,j)) = (a * (i,j)) + (b * (i,j))

proof

A7: A * (i,j) = a * (i,j) by A1, A3, A5, Th83;
Indices B = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (a + b) by MATRIX_0:24 ;
then B * (i,j) = b * (i,j) by A2, A3, Th83;
hence (A * (i,j)) + (B * (i,j)) = (a * (i,j)) + (b * (i,j)) by A7, FIELD_6:15; :: thesis: verum

end;

thus (a + b) * (i,j) = (a * (i,j)) + (b * (i,j)) by A3, A4, MATRIX_1:def 8
.= (A + B) * (i,j) by A3, A5, A6, MATRIX_1:def 8 ; :: thesis: verum

end;

hence a + b = A + B by Th83; :: thesis: verum