begin
definition
let M be
Matrix of
REAL;
existence
ex b1 being Matrix of REAL st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = abs (M * (i,j)) ) )
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = abs (M * (i,j)) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = abs (M * (i,j)) ) holds
b1 = b2
end;
Lm1:
for n being Nat
for M1, M2 being Matrix of n, REAL holds
( len M1 = len M2 & width M1 = width M2 )
begin