A1: ( len A = len A & width A = width A ) ;
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (1. K) * (A * (i,j)) ;
hence (1. K) * A = A by A1, Def5; :: thesis: verum