let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @ ) + (M2 @ )
let K be Field; :: thesis: for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @ ) + (M2 @ )
let M1, M2 be Matrix of n,K; :: thesis: (M1 + M2) @ = (M1 @ ) + (M2 @ )
for i, j being Nat st [i,j] in Indices ((M1 + M2) @ ) holds
((M1 + M2) @ ) * i,j = ((M1 @ ) + (M2 @ )) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((M1 + M2) @ ) implies ((M1 + M2) @ ) * i,j = ((M1 @ ) + (M2 @ )) * i,j )
assume [i,j] in Indices ((M1 + M2) @ ) ; :: thesis: ((M1 + M2) @ ) * i,j = ((M1 @ ) + (M2 @ )) * i,j
then A1: [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:25;
then A2: [i,j] in Indices (M1 @ ) by MATRIX_1:25;
( i in Seg n & j in Seg n ) by A1, ZFMISC_1:106;
then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:106;
then A4: [j,i] in Indices M1 by MATRIX_1:25;
A5: [j,i] in Indices M2 by A3, MATRIX_1:25;
[j,i] in Indices (M1 + M2) by A3, MATRIX_1:25;
then ((M1 + M2) @ ) * i,j = (M1 + M2) * j,i by MATRIX_1:def 7
.= (M1 * j,i) + (M2 * j,i) by A4, MATRIX_3:def 3
.= ((M1 @ ) * i,j) + (M2 * j,i) by A4, MATRIX_1:def 7
.= ((M1 @ ) * i,j) + ((M2 @ ) * i,j) by A5, MATRIX_1:def 7
.= ((M1 @ ) + (M2 @ )) * i,j by A2, MATRIX_3:def 3 ;
hence ((M1 + M2) @ ) * i,j = ((M1 @ ) + (M2 @ )) * i,j ; :: thesis: verum

end;

hence (M1 + M2) @ = (M1 @ ) + (M2 @ ) by MATRIX_1:28; :: thesis: verum