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 j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= 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 j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )

hereby :: thesis: ( ( for i, j being Nat st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= 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 j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r

hereby :: thesis: verum

let i, j be Nat; :: thesis: ( j in Seg (width m) & i in dom (Col (m,j)) implies (Col (m,j)) . i >= r )
assume that
A2: j in Seg (width m) and
A3: i in dom (Col (m,j)) ; :: thesis: (Col (m,j)) . i >= r
j in Seg (len (Line (m,i))) by A2, MATRIX_0:def 7;
then A4: j in dom (Line (m,i)) by FINSEQ_1:def 3;
then [i,j] in Indices m by A3, Th15;
then A5: i in dom m by Th13;
then (Line (m,i)) . j >= r by A1, A4, Lm2;
hence (Col (m,j)) . i >= r by A2, A5, MATRIX_0:42; :: thesis: verum

end;

end;

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

proof

let i, j be Nat; :: thesis: ( i in dom m & j in dom (Line (m,i)) implies (Line (m,i)) . j >= r )
assume that
A7: i in dom m and
A8: j in dom (Line (m,i)) ; :: thesis: (Line (m,i)) . j >= r
j in Seg (len (Line (m,i))) by A8, FINSEQ_1:def 3;
then A9: j in Seg (width m) by MATRIX_0:def 7;
i in Seg (len m) by A7, FINSEQ_1:def 3;
then i in Seg (len (Col (m,j))) by MATRIX_0:def 8;
then i in dom (Col (m,j)) by FINSEQ_1:def 3;
then (Col (m,j)) . i >= r by A6, A9;
hence (Line (m,i)) . j >= r by A7, A9, MATRIX_0:42; :: thesis: verum

end;

hence for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r by Lm2; :: thesis: verum