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

hereby :: thesis: ( ( for i, j being Element of NAT st i in dom m & j in dom (Line m,i) holds
(Line m,i) . j >= r ) implies for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r )

assume A1: for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r ; :: thesis: for i, j being Element of NAT st i in dom m & j in dom (Line m,i) holds
(Line m,i) . j >= r

hereby :: thesis: verum

let i, j be Element of NAT ; :: thesis: ( i in dom m & j in dom (Line m,i) implies (Line m,i) . j >= r )
assume A2: ( i in dom m & j in dom (Line m,i) ) ; :: thesis: (Line m,i) . j >= r
m . i = Line m,i by A2, MATRIX_2:18;
hence (Line m,i) . j >= r by A1, A2, Lm1; :: thesis: verum

end;

end;

assume A3: for i, j being Element of NAT st i in dom m & j in dom (Line m,i) holds
(Line m,i) . j >= r ; :: thesis: for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r

now

let i be Element of NAT ; :: thesis: ( i in dom m implies for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r )
assume A4: i in dom m ; :: thesis: for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r
m . i = Line m,i by A4, MATRIX_2:18;
hence for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r by A3, A4; :: thesis: verum

end;

then for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r ;
hence for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r by Lm1; :: thesis: verum