let n, m be non zero Nat; :: thesis: ex M being Matrix of n,m,REAL st
( M is m-nonnegative & M is with_line_sum=1 )
consider m1 being Nat such that
A1: m = m1 + 1 by NAT_1:6;
reconsider m1 = m1 as Nat ;
consider e1 being FinSequence of REAL such that
A2: len e1 = m and
A3: for i being Nat st i in Seg m holds
( ( i in Seg m1 implies e1 . i = zz ) & ( not i in Seg m1 implies e1 . i = jj ) ) by Th2;
m1 + 1 > m1 by NAT_1:13;
then A4: not m1 + 1 in Seg m1 by FINSEQ_1:1;
m1 + 1 in Seg m by A1, FINSEQ_1:4;
then e1 . (m1 + 1) = 1 by A3, A4;
then A5: e1 = (e1 | m1) ^ <*1*> by A1, A2, RFINSEQ:7;
reconsider M1 = n |-> e1 as Matrix of n,m,REAL by A2, Th18;
A6: len M1 = n by MATRIX_0:def 2;
A7: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) >= 0

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume A8: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) >= 0
consider p1 being FinSequence of REAL such that
A9: p1 = M1 . i and
A10: M1 * (i,j) = p1 . j by A8, MATRIX_0:def 5;
A11: [i,j] in [:(dom M1),(Seg (width M1)):] by A8, MATRIX_0:def 4;
then j in Seg (width M1) by ZFMISC_1:87;
then A12: j in Seg m by A6, MATRIX_0:20;
i in dom M1 by A11, ZFMISC_1:87;
then i in Seg n by A6, FINSEQ_1:def 3;
then p1 = e1 by A9, FUNCOP_1:7;
hence M1 * (i,j) >= 0 by A3, A10, A12; :: thesis: verum

end;

reconsider e3 = e1 | m1 as FinSequence of REAL ;
m > m1 by A1, NAT_1:13;
then A13: len e3 = m1 by A2, FINSEQ_1:59;
take M1 ; :: thesis: ( M1 is m-nonnegative & M1 is with_line_sum=1 )
A14: dom e1 = Seg m by A2, FINSEQ_1:def 3;
A15: Sum e1 = 1

proof

per cases ( m1 = 0 or m1 <> 0 ) ;

suppose m1 = 0 ; :: thesis: Sum e1 = 1

then A16: e3 = <*> REAL ;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A5, RVSUM_1:74
.= 1 by A16, RVSUM_1:72 ; :: thesis: verum

end;

suppose A17: m1 <> 0 ; :: thesis: Sum e1 = 1

for i being Nat st i in dom e3 holds
e3 . i = 0

proof

let i be Nat; :: thesis: ( i in dom e3 implies e3 . i = 0 )
assume i in dom e3 ; :: thesis: e3 . i = 0
then A18: i in Seg m1 by A13, FINSEQ_1:def 3;
m1 + 1 in Seg (m1 + 1) by FINSEQ_1:4;
then m1 in Seg m by A1, A17, FINSEQ_1:61;
then m1 in dom e1 by A2, FINSEQ_1:def 3;
then ( e3 . i = e1 . i & i in dom e1 ) by A18, RFINSEQ:6;
hence e3 . i = 0 by A3, A14, A18; :: thesis: verum

end;

then e3 = m1 |-> 0 by A13, A17, Th1, Lm4;
then A19: Sum e3 = m1 * 0 by RVSUM_1:80
.= 0 ;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A5, RVSUM_1:74
.= 1 by A19 ; :: thesis: verum

end;

end;

end;

for i being Nat st i in dom M1 holds
Sum (M1 . i) = 1

proof

let i be Nat; :: thesis: ( i in dom M1 implies Sum (M1 . i) = 1 )
assume i in dom M1 ; :: thesis: Sum (M1 . i) = 1
then i in Seg n by A6, FINSEQ_1:def 3;
hence Sum (M1 . i) = 1 by A15, FUNCOP_1:7; :: thesis: verum

end;

hence ( M1 is m-nonnegative & M1 is with_line_sum=1 ) by A7; :: thesis: verum