let MR be Matrix of REAL ; :: thesis: ( MR is m-nonnegative iff for i being Element of NAT st i in dom MR holds
Line MR,i is nonnegative )

hereby :: thesis: ( ( for i being Element of NAT st i in dom MR holds
Line MR,i is nonnegative ) implies MR is m-nonnegative )

assume A1: MR is m-nonnegative ; :: thesis: for i being Element of NAT st i in dom MR holds
Line MR,i is nonnegative
let i be Element of NAT ; :: thesis: ( i in dom MR implies Line MR,i is nonnegative )
assume A2: i in dom MR ; :: thesis: Line MR,i is nonnegative

now

let k be Element of NAT ; :: thesis: ( k in dom (Line MR,i) implies (Line MR,i) . k >= 0 )
assume k in dom (Line MR,i) ; :: thesis: (Line MR,i) . k >= 0
then A3: k in dom (MR . i) by A2, MATRIX_2:18;
then k in Seg (width MR) by A2, Th18;
then A4: (Line MR,i) . k = MR * i,k by MATRIX_1:def 8;
[i,k] in Indices MR by A2, A3, MATRPROB:13;
hence (Line MR,i) . k >= 0 by A1, A4, MATRPROB:def 6; :: thesis: verum

end;

hence Line MR,i is nonnegative by Def1; :: thesis: verum

end;

assume A5: for i being Element of NAT st i in dom MR holds
Line MR,i is nonnegative ; :: thesis: MR is m-nonnegative

now

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices MR implies MR * i,j >= 0 )
assume A6: [i,j] in Indices MR ; :: thesis: MR * i,j >= 0
A7: j in Seg (width MR) by A6, MATRPROB:12;
then j in Seg (len (Line MR,i)) by MATRIX_1:def 8;
then A8: j in dom (Line MR,i) by FINSEQ_1:def 3;
i in Seg (len MR) by A6, MATRPROB:12;
then i in dom MR by FINSEQ_1:def 3;
then A9: Line MR,i is nonnegative by A5;
MR * i,j = (Line MR,i) . j by A7, MATRIX_1:def 8;
hence MR * i,j >= 0 by A8, A9, Def1; :: thesis: verum

end;

hence MR is m-nonnegative by MATRPROB:def 6; :: thesis: verum