let n, m be non empty 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 Element of NAT by ORDINAL1:def 13;
consider e1 being FinSequence of REAL such that
A2: ( len e1 = m & ( for i being Nat st i in Seg m holds
( ( i in Seg m1 implies e1 . i = 0 ) & ( not i in Seg m1 implies e1 . i = 1 ) ) ) ) by Th2;
reconsider M1 = n |-> e1 as Matrix of n,m, REAL by A2, Th18;
take M1 ; :: thesis: ( M1 is m-nonnegative & M1 is with_line_sum=1 )
A3: dom e1 = Seg m by A2, FINSEQ_1:def 3;
A4: m1 + 1 in Seg m by A1, FINSEQ_1:6;
A5: ( m1 + 1 > m1 & m > m1 ) by A1, NAT_1:13;
then not m1 + 1 in Seg m1 by FINSEQ_1:3;
then ( e1 . (m1 + 1) = 1 & len e1 = m1 + 1 ) by A1, A2, A4;
then A6: e1 = (e1 | m1) ^ <*1*> by RFINSEQ:20;
reconsider e3 = e1 | m1 as FinSequence of REAL ;
A7: len e3 = m1 by A2, A5, FINSEQ_1:80;
A8: Sum e1 = 1

proof

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

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

then A9: e3 = <*> REAL ;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A6, RVSUM_1:104
.= 1 by A9, RVSUM_1:102 ; :: thesis: verum

end;

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

then A11: m1 > 0 ;
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 A12: i in Seg m1 by A7, FINSEQ_1:def 3;
m1 + 1 in Seg (m1 + 1) by FINSEQ_1:6;
then m1 in Seg m by A1, A11, FINSEQ_1:82;
then m1 in dom e1 by A2, FINSEQ_1:def 3;
then ( e3 . i = e1 . i & i in dom e1 ) by A12, RFINSEQ:19;
hence e3 . i = 0 by A2, A3, A12; :: thesis: verum

end;

then e3 = m1 |-> 0 by A7, A10, Th1;
then A13: Sum e3 = m1 * 0 by RVSUM_1:110
.= 0 ;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A6, RVSUM_1:104
.= 1 by A13 ; :: thesis: verum

end;

end;

end;

A14: ( len M1 = n & len M1 <> 0 ) by MATRIX_1:def 3;
A15: for i being Element of NAT st i in dom M1 holds
Sum (M1 . i) = 1

proof

let i be Element of NAT ; :: thesis: ( i in dom M1 implies Sum (M1 . i) = 1 )
assume A16: i in dom M1 ; :: thesis: Sum (M1 . i) = 1
i in Seg n by A14, A16, FINSEQ_1:def 3;
hence Sum (M1 . i) = 1 by A8, FUNCOP_1:13; :: thesis: verum

end;

for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j >= 0

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M1 implies M1 * i,j >= 0 )
assume A17: [i,j] in Indices M1 ; :: thesis: M1 * i,j >= 0
consider p1 being FinSequence of REAL such that
A18: ( p1 = M1 . i & M1 * i,j = p1 . j ) by A17, MATRIX_1:def 6;
[i,j] in [:(dom M1),(Seg (width M1)):] by A17, MATRIX_1:def 5;
then A19: ( i in dom M1 & j in Seg (width M1) ) by ZFMISC_1:106;
then i in Seg n by A14, FINSEQ_1:def 3;
then A20: p1 = e1 by A18, FUNCOP_1:13;
j in Seg m by A14, A19, MATRIX_1:20;
hence M1 * i,j >= 0 by A2, A18, A20; :: thesis: verum

end;

hence ( M1 is m-nonnegative & M1 is with_line_sum=1 ) by A15, Def6, Def9; :: thesis: verum