let r be Real; for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
let m be Matrix of REAL; ( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
assume A3:
for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r
; for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r