let n, m be non empty 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 m1 = m1, n1 = n1 as Element of NAT by ORDINAL1:def 13;
reconsider n = n, m = m as non empty Element of NAT by ORDINAL1:def 13;
consider e1 being FinSequence of REAL such that
A3: ( 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 e2 = m |-> 0 as FinSequence of REAL ;
A4: ( len e2 = m & ( for i being Nat st i in Seg m holds
e2 . i = 0 ) ) by FINSEQ_1:def 18, FUNCOP_1:13;
then consider M1 being Matrix of n,m, REAL such that
A5: 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;
A6: ( dom e2 = Seg m & dom e1 = Seg m ) by A3, A4, FINSEQ_1:def 3;
A7: Sum e2 = m * 0 by RVSUM_1:110
.= 0 ;
A8: m1 + 1 in Seg m by A1, FINSEQ_1:6;
A9: ( 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, A3, A8;
then A10: e1 = (e1 | m1) ^ <*1*> by RFINSEQ:20;
reconsider e3 = e1 | m1 as FinSequence of REAL ;
A11: len e3 = m1 by A3, A9, FINSEQ_1:80;
A12: Sum e1 = 1

proof

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

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

then len e3 = 0 ;
then A13: Sum e3 = 0 by FINSEQ_1:32, RVSUM_1:102;
thus Sum e1 = (Sum (e1 | m1)) + 1 by A10, RVSUM_1:104
.= 1 by A13 ; :: thesis: verum

end;

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

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

end;

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

end;

end;

end;

A19: ( len (Sum M1) = n & ( for i being Element of 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 A20: len (Sum M1) = len M1 by Def1
.= n by MATRIX_1:def 3 ; :: thesis: for i being Element of 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 Element of 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 A21: i in Seg n ; :: thesis: ( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) )
A22: i in dom (Sum M1) by A20, A21, 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 A23: i in Seg n1 ; :: thesis: (Sum M1) . i = 0
thus (Sum M1) . i = Sum (M1 . i) by A22, Def1
.= 0 by A5, A7, A21, A23 ; :: thesis: verum

end;

assume A24: not i in Seg n1 ; :: thesis: (Sum M1) . i = 1
thus (Sum M1) . i = Sum (M1 . i) by A22, Def1
.= 1 by A5, A12, A21, A24 ; :: thesis: verum

end;

A25: SumAll M1 = 1

proof

reconsider e4 = Sum M1 as FinSequence of REAL ;
A26: dom e4 = Seg n by A19, FINSEQ_1:def 3;
A27: n1 + 1 in Seg n by A2, FINSEQ_1:6;
A28: ( n1 + 1 > n1 & n > n1 ) by A2, NAT_1:13;
then not n1 + 1 in Seg n1 by FINSEQ_1:3;
then A29: ( e4 . (n1 + 1) = 1 & len e4 = n1 + 1 ) by A2, A19, A27;
reconsider e5 = e4 | n1 as FinSequence of REAL ;
A30: len e5 = n1 by A19, A28, FINSEQ_1:80;
Sum e4 = 1

proof

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

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

then len e5 = 0 ;
then A31: e5 = <*> REAL ;
thus Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A29, RFINSEQ:20
.= (Sum (e4 | n1)) + 1 by RVSUM_1:104
.= 1 by A31, RVSUM_1:102 ; :: thesis: verum

end;

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

then A33: n1 > 0 ;
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 A34: i in dom e5 ; :: thesis: e5 . i = 0
A35: i in Seg n1 by A30, A34, FINSEQ_1:def 3;
n1 + 1 in Seg (n1 + 1) by FINSEQ_1:6;
then n1 in Seg n by A2, A33, FINSEQ_1:82;
then n1 in dom e4 by A19, FINSEQ_1:def 3;
then ( e5 . i = e4 . i & i in dom e4 ) by A35, RFINSEQ:19;
hence e5 . i = 0 by A19, A26, A35; :: thesis: verum

end;

then e5 = n1 |-> 0 by A30, A32, Th1;
then A36: Sum e5 = n1 * 0 by RVSUM_1:110
.= 0 ;
thus Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A29, RFINSEQ:20
.= (Sum (e4 | n1)) + 1 by RVSUM_1:104
.= 1 by A36 ; :: thesis: verum

end;

end;

end;

hence SumAll M1 = 1 ; :: 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 A37: [i,j] in Indices M1 ; :: thesis: M1 * i,j >= 0
consider p1 being FinSequence of REAL such that
A38: ( p1 = M1 . i & M1 * i,j = p1 . j ) by A37, MATRIX_1:def 6;
[i,j] in [:(dom M1),(Seg (width M1)):] by A37, MATRIX_1:def 5;
then A39: ( i in dom M1 & j in Seg (width M1) ) by ZFMISC_1:106;
A40: ( len M1 = n & len M1 <> 0 ) by MATRIX_1:def 3;
then A41: i in Seg n by A39, FINSEQ_1:def 3;
A42: j in Seg m by A39, A40, MATRIX_1:20;

per cases ( p1 = e2 or p1 = e1 ) by A5, A38, A41;

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

hence M1 * i,j >= 0 by A38; :: thesis: verum

end;

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

hence M1 * i,j >= 0 by A3, A38, A42; :: thesis: verum

end;

end;

end;

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