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 (m . i) holds
(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 (m . i) holds
(m . i) . j >= r )

hereby :: thesis: ( ( for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(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 (m . i) holds
(m . i) . j >= r

hereby :: thesis: verum

let i, j be Element of NAT ; :: thesis: ( i in dom m & j in dom (m . i) implies (m . i) . j >= r )
assume A2: ( i in dom m & j in dom (m . i) ) ; :: thesis: (m . i) . j >= r
[i,j] in Indices m by A2, Th13;
then ( m * i,j >= r & m * i,j = (m . i) . j ) by A1, Th14;
hence (m . i) . j >= r ; :: thesis: verum

end;

end;

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

hereby :: thesis: verum

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices m implies m * i,j >= r )
assume A4: [i,j] in Indices m ; :: thesis: m * i,j >= r
( i in dom m & j in dom (m . i) ) by A4, Th13;
then ( (m . i) . j >= r & m * i,j = (m . i) . j ) by A3, A4, Th14;
hence m * i,j >= r ; :: thesis: verum

end;