let R be Ring; :: thesis: for x, y being Element of R
for M1, M2 being Matrix of 1,R st M1 = <*<*x*>*> & M2 = <*<*y*>*> holds
M1 + M2 = <*<*(x + y)*>*>
let x, y be Element of R; :: thesis: for M1, M2 being Matrix of 1,R st M1 = <*<*x*>*> & M2 = <*<*y*>*> holds
M1 + M2 = <*<*(x + y)*>*>
let M1, M2 be Matrix of 1,R; :: thesis: ( M1 = <*<*x*>*> & M2 = <*<*y*>*> implies M1 + M2 = <*<*(x + y)*>*> )
assume A1: M1 = <*<*x*>*> ; :: thesis: ( not M2 = <*<*y*>*> or M1 + M2 = <*<*(x + y)*>*> )
assume A2: M2 = <*<*y*>*> ; :: thesis: M1 + M2 = <*<*(x + y)*>*>
A3: ( Indices (M1 + M2) = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:2, MATRIX_0:24, TARSKI:def 1;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = <*<*(x + y)*>*> * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = <*<*(x + y)*>*> * (i,j) )
assume A4: [i,j] in Indices (M1 + M2) ; :: thesis: (M1 + M2) * (i,j) = <*<*(x + y)*>*> * (i,j)
then ( i in Seg 1 & j in Seg 1 ) by A3, ZFMISC_1:87;
then A5: ( i = 1 & j = 1 ) by FINSEQ_1:2, TARSKI:def 1;
[i,j] in Indices M1 by A3, A4, MATRIX_0:24;
hence (M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by MATRIX_1:def 8
.= x + (<*<*y*>*> * (1,1)) by A1, A2, A5, MATRIX_0:49
.= x + y by MATRIX_0:49
.= <*<*(x + y)*>*> * (i,j) by A5, MATRIX_0:49 ;
:: thesis: verum

end;

hence M1 + M2 = <*<*(x + y)*>*> by MATRIX_0:27; :: thesis: verum