let r be Real; :: thesis: 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; :: thesis: ( ( 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 )

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

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

hereby :: thesis: verum

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

end;

end;

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

hereby :: thesis: verum

let i, j be 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 by A3;
hence m * (i,j) >= r by A4, Th14; :: thesis: verum

end;