let MR be Matrix of REAL; :: thesis: ( MR is m-nonnegative iff Mx2FinS MR is nonnegative )

hereby :: thesis: ( Mx2FinS MR is nonnegative implies MR is m-nonnegative )

assume A1: MR is m-nonnegative ; :: thesis: Mx2FinS MR is nonnegative
for k being Element of NAT st k in dom (Mx2FinS MR) holds
(Mx2FinS MR) . k >= 0

proof

let i be Element of NAT ; :: thesis: ( i in dom (Mx2FinS MR) implies (Mx2FinS MR) . i >= 0 )
assume A2: i in dom (Mx2FinS MR) ; :: thesis: (Mx2FinS MR) . i >= 0
i in Seg (len (Mx2FinS MR)) by A2, FINSEQ_1:def 3;
then i >= 1 by FINSEQ_1:1;
then reconsider l = i - 1 as Element of NAT by NAT_1:21;
A3: (Mx2FinS MR) . i = MR * (((l div (width MR)) + 1),((l mod (width MR)) + 1)) by A2, Th41;
[((l div (width MR)) + 1),((l mod (width MR)) + 1)] in Indices MR by A2, Th41;
hence (Mx2FinS MR) . i >= 0 by A1, A3, MATRPROB:def 6; :: thesis: verum

end;

hence Mx2FinS MR is nonnegative by Def1; :: thesis: verum

end;

assume A4: Mx2FinS MR 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 A5: [i,j] in Indices MR ; :: thesis: MR * (i,j) >= 0
A6: MR * (i,j) = (Mx2FinS MR) . (((i - 1) * (width MR)) + j) by A5, Th40;
((i - 1) * (width MR)) + j in dom (Mx2FinS MR) by A5, Th40;
hence MR * (i,j) >= 0 by A4, A6, Def1; :: thesis: verum

end;

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