let n be Nat; :: thesis: for K being Field
for a9, b9 being Element of K holds (n,n --> a9) + (n,n --> b9) = n,n --> (a9 + b9)
let K be Field; :: thesis: for a9, b9 being Element of K holds (n,n --> a9) + (n,n --> b9) = n,n --> (a9 + b9)
let a9, b9 be Element of K; :: thesis: (n,n --> a9) + (n,n --> b9) = n,n --> (a9 + b9)
A1: Indices (n,n --> a9) = Indices (n,n --> (a9 + b9)) by MATRIX_1:27;
A2: Indices (n,n --> a9) = Indices (n,n --> b9) by MATRIX_1:27;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (n,n --> (a9 + b9)) implies ((n,n --> a9) * i,j) + ((n,n --> b9) * i,j) = (n,n --> (a9 + b9)) * i,j )
assume A3: [i,j] in Indices (n,n --> (a9 + b9)) ; :: thesis: ((n,n --> a9) * i,j) + ((n,n --> b9) * i,j) = (n,n --> (a9 + b9)) * i,j
then (n,n --> a9) * i,j = a9 by A1, Th1;
then ((n,n --> a9) * i,j) + ((n,n --> b9) * i,j) = a9 + b9 by A2, A1, A3, Th1;
hence ((n,n --> a9) * i,j) + ((n,n --> b9) * i,j) = (n,n --> (a9 + b9)) * i,j by A3, Th1; :: thesis: verum

end;

hence (n,n --> a9) + (n,n --> b9) = n,n --> (a9 + b9) by A1, MATRIX_1:def 14; :: thesis: verum