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 & i <= len (Mx2FinS MR) ) by FINSEQ_1:3;
then reconsider l = i - 1 as Element of NAT by NAT_1:21;
( [((l div (width MR)) + 1),((l mod (width MR)) + 1)] in Indices MR & (Mx2FinS MR) . i = MR * ((l div (width MR)) + 1),((l mod (width MR)) + 1) ) by A2, Th41;
hence (Mx2FinS MR) . i >= 0 by A1, MATRPROB:def 6; :: thesis: verum

end;

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

end;

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

end;

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