let MR be Matrix of REAL; ( MR is m-nonnegative iff Mx2FinS MR is nonnegative )
assume A4:
Mx2FinS MR is nonnegative
; MR is m-nonnegative
now for i, j being Nat st [i,j] in Indices MR holds
MR * (i,j) >= 0 let i,
j be
Nat;
( [i,j] in Indices MR implies MR * (i,j) >= 0 )assume A5:
[i,j] in Indices MR
;
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;
verum end;
hence
MR is m-nonnegative
by MATRPROB:def 6; verum