let n, m be non zero Nat; :: thesis: ex M being Matrix of n,m,REAL st
( M is m-nonnegative & SumAll M = 1 )
consider m1 being Nat such that
A1: m = m1 + 1 by NAT_1:6;
consider n1 being Nat such that
A2: n = n1 + 1 by NAT_1:6;
reconsider n = n, m = m as non zero Nat ;
reconsider m1 = m1, n1 = n1 as Nat ;
consider e1 being FinSequence of REAL such that
A3: len e1 = m and
A4: 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 A5: 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 A4, A5;
then A6: e1 = (e1 | m1) ^ <*1*> by A1, A3, RFINSEQ:7;
reconsider e3 = e1 | m1 as FinSequence of REAL ;
m > m1 by A1, NAT_1:13;
then A7: len e3 = m1 by A3, FINSEQ_1:59;
A8: dom e1 = Seg m by A3, FINSEQ_1:def 3;
A9: Sum e1 = 1

proof

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

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

then A10: Sum e3 = 0 by RVSUM_1:72;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A6, RVSUM_1:74
.= 1 by A10 ; :: thesis: verum

end;

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

end;

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

end;

end;

end;

reconsider e2 = m |-> (In (0,REAL)) as FinSequence of REAL ;
len e2 = m by CARD_1:def 7;
then consider M1 being Matrix of n,m,REAL such that
A14: for i being Nat st i in Seg n holds
( ( i in Seg n1 implies M1 . i = e2 ) & ( not i in Seg n1 implies M1 . i = e1 ) ) by A3, Th19;
A15: Sum e2 = m * 0 by RVSUM_1:80
.= 0 ;
A16: ( len (Sum M1) = n & ( for i being Nat st i in Seg n holds
( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) ) ) )

proof

thus A17: len (Sum M1) = len M1 by Def1
.= n by MATRIX_0:def 2 ; :: thesis: for i being Nat st i in Seg n holds
( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) )
let i be Nat; :: thesis: ( i in Seg n implies ( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) ) )
assume A18: i in Seg n ; :: thesis: ( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) )
A19: i in dom (Sum M1) by A17, A18, FINSEQ_1:def 3;
thus ( i in Seg n1 implies (Sum M1) . i = 0 ) :: thesis: ( not i in Seg n1 implies (Sum M1) . i = 1 )

proof

assume A20: i in Seg n1 ; :: thesis: (Sum M1) . i = 0
thus (Sum M1) . i = Sum (M1 . i) by A19, Def1
.= 0 by A14, A15, A18, A20 ; :: thesis: verum

end;

assume A21: not i in Seg n1 ; :: thesis: (Sum M1) . i = 1
thus (Sum M1) . i = Sum (M1 . i) by A19, Def1
.= 1 by A14, A9, A18, A21 ; :: thesis: verum

end;

A22: SumAll M1 = 1

proof

reconsider e4 = Sum M1 as FinSequence of REAL ;
reconsider e5 = e4 | n1 as FinSequence of REAL ;
n1 + 1 > n1 by NAT_1:13;
then A23: not n1 + 1 in Seg n1 by FINSEQ_1:1;
n1 + 1 in Seg n by A2, FINSEQ_1:4;
then A24: e4 . (n1 + 1) = 1 by A16, A23;
n > n1 by A2, NAT_1:13;
then A25: len e5 = n1 by A16, FINSEQ_1:59;
A26: dom e4 = Seg n by A16, FINSEQ_1:def 3;
Sum e4 = 1

proof

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

suppose n1 = 0 ; :: thesis: Sum e4 = 1

then A27: e5 = <*> REAL ;
thus Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A2, A16, A24, RFINSEQ:7
.= (Sum (e4 | n1)) + 1 by RVSUM_1:74
.= 1 by A27, RVSUM_1:72 ; :: thesis: verum

end;

suppose A28: n1 <> 0 ; :: thesis: Sum e4 = 1

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

proof

let i be Nat; :: thesis: ( i in dom e5 implies e5 . i = 0 )
assume i in dom e5 ; :: thesis: e5 . i = 0
then A29: i in Seg n1 by A25, FINSEQ_1:def 3;
n1 + 1 in Seg (n1 + 1) by FINSEQ_1:4;
then n1 in Seg n by A2, A28, FINSEQ_1:61;
then n1 in dom e4 by A16, FINSEQ_1:def 3;
then ( e5 . i = e4 . i & i in dom e4 ) by A29, RFINSEQ:6;
hence e5 . i = 0 by A16, A26, A29; :: thesis: verum

end;

then e5 = n1 |-> 0 by A25, A28, Th1, Lm4;
then A30: Sum e5 = n1 * 0 by RVSUM_1:80
.= 0 ;
thus Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A2, A16, A24, RFINSEQ:7
.= (Sum (e4 | n1)) + 1 by RVSUM_1:74
.= 1 by A30 ; :: thesis: verum

end;

end;

end;

hence SumAll M1 = 1 ; :: thesis: verum

end;

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 A31: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) >= 0
consider p1 being FinSequence of REAL such that
A32: p1 = M1 . i and
A33: M1 * (i,j) = p1 . j by A31, MATRIX_0:def 5;
A34: len M1 = n by MATRIX_0:def 2;
A35: [i,j] in [:(dom M1),(Seg (width M1)):] by A31, MATRIX_0:def 4;
then i in dom M1 by ZFMISC_1:87;
then A36: i in Seg n by A34, FINSEQ_1:def 3;
j in Seg (width M1) by A35, ZFMISC_1:87;
then A37: j in Seg m by A34, MATRIX_0:20;

per cases ( p1 = e2 or p1 = e1 ) by A14, A32, A36;

suppose p1 = e2 ; :: thesis: M1 * (i,j) >= 0

hence M1 * (i,j) >= 0 by A33; :: thesis: verum

end;

suppose p1 = e1 ; :: thesis: M1 * (i,j) >= 0

hence M1 * (i,j) >= 0 by A4, A33, A37; :: thesis: verum

end;

end;

end;

then M1 is m-nonnegative ;
hence ex M being Matrix of n,m,REAL st
( M is m-nonnegative & SumAll M = 1 ) by A22; :: thesis: verum