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 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 Element of NAT st [i,j] in Indices m holds
m * i,j >= r ) iff for i, j being Element of 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 Element of NAT st j in Seg (width m) & i in dom (Col m,j) holds
(Col m,j) . i >= 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 j in Seg (width m) & i in dom (Col m,j) holds
(Col m,j) . i >= r

hereby :: thesis: verum

let i, j be Element of NAT ; :: thesis: ( j in Seg (width m) & i in dom (Col m,j) implies (Col m,j) . i >= r )
assume A2: ( j in Seg (width m) & i in dom (Col m,j) ) ; :: thesis: (Col m,j) . i >= r
j in Seg (len (Line m,i)) by A2, MATRIX_1:def 8;
then A3: j in dom (Line m,i) by FINSEQ_1:def 3;
then [i,j] in Indices m by A2, Th15;
then A4: i in dom m by Th13;
then (Line m,i) . j >= r by A1, A3, Lm2;
hence (Col m,j) . i >= r by A2, A4, GOBOARD1:17; :: thesis: verum

end;

end;

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

proof

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 A6: ( i in dom m & j in dom (Line m,i) ) ; :: thesis: (Line m,i) . j >= r
j in Seg (len (Line m,i)) by A6, FINSEQ_1:def 3;
then A7: j in Seg (width m) by MATRIX_1:def 8;
i in Seg (len m) by A6, FINSEQ_1:def 3;
then i in Seg (len (Col m,j)) by MATRIX_1:def 9;
then i in dom (Col m,j) by FINSEQ_1:def 3;
then (Col m,j) . i >= r by A5, A7;
hence (Line m,i) . j >= r by A6, A7, GOBOARD1:17; :: thesis: verum

end;

hence for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r by Lm2; :: thesis: verum