let MR be Matrix of REAL; :: thesis: ( MR is m-nonnegative iff for i being Nat st i in dom MR holds
Line (MR,i) is nonnegative )
hereby :: thesis: ( ( for i being 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 Nat st i in dom MR holds
Line (MR,i) is nonnegative
let i be 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 :: thesis: for k being Nat st k in dom (Line (MR,i)) holds
(Line (MR,i)) . k >= 0
let k be 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_0:60;
then k in Seg (width MR) by A2, Th18;
then A4: (Line (MR,i)) . k = MR * (i,k) by MATRIX_0:def 7;
[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 ; :: thesis: verum
end;
assume A5: for i being Nat st i in dom MR holds
Line (MR,i) is nonnegative ; :: thesis: MR is m-nonnegative
now :: thesis: for i, j being Nat st [i,j] in Indices MR holds
MR * (i,j) >= 0
let i, j be 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_0:def 7;
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_0:def 7;
hence MR * (i,j) >= 0 by A8, A9; :: thesis: verum
end;
hence MR is m-nonnegative by MATRPROB:def 6; :: thesis: verum