let R be Ring; :: thesis: for n, i, j being Nat
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )
let n be Nat; :: thesis: for i, j being Nat
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )
let i, j be Nat; :: thesis: for A being Matrix of n,R holds
( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )
let A be Matrix of n,R; :: thesis: ( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )
(1. R) * (canMat (i,j,n,R)) = canMat (i,j,n,R) ;
hence ( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A ) by Th58; :: thesis: verum