:: The Definition of Finite Sequences and Matrices of Probability, and Addition of Matrices of Real Elements
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

definition
let d be set ;
let g be FinSequence of d * ;
let n be Nat;
:: original:.
redefine funcg . n ->  FinSequence of d;
correctness
coherence
g . n is FinSequence of d;
proofend;
end;

definition
let x be real number ;
:: original:<*
redefine func<*x*> ->  FinSequence of REAL ;
coherence
 <*x*> is FinSequence of REAL
proofend;
end;

theorem Th1: :: MATRPROB:1
for D being non empty set
for a being Element of D
for m being non empty Nat
for g being FinSequence of D holds
( ( len g = m &amp; ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
proofend;

theorem Th2: :: MATRPROB:2
for D being non empty set
for k being Element of NAT
for n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n &amp; ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) &amp; ( not i in Seg k implies g . i = b ) ) ) )
proofend;

theorem Th3: :: MATRPROB:3
for e being FinSequence of REAL st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st ( for n being Nat st 0 <> n &amp; n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e &amp; m in dom e &amp; n <= m holds
f . n <= f . m
proofend;

theorem Th4: :: MATRPROB:4
for e being FinSequence of REAL st len e >= 1 &amp; ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st f . 1 = e . 1 &amp; ( for n being Nat st 0 <> n &amp; n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n being Nat st n in dom e holds
e . n <= f . n
proofend;

theorem Th5: :: MATRPROB:5
for e being FinSequence of REAL st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for k being Nat st k in dom e holds
e . k <= Sum e
proofend;

theorem Th6: :: MATRPROB:6
for r1, r2 being Real
for k being Nat
for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 &amp; ( for n being Nat holds
( ( n <> 0 &amp; n <= k implies seq . n = seq1 . n ) &amp; ( n > k implies seq . n = r2 ) ) ) )
proofend;

theorem Th7: :: MATRPROB:7
for F being FinSequence of REAL ex f being Real_Sequence st
( f . 0 = 0 &amp; ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) &amp; Sum F = f . (len F) )
proofend;

theorem Th8: :: MATRPROB:8
for n being Nat
for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
proofend;

theorem Th9: :: MATRPROB:9
for k being Element of NAT
for n being Nat
for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n &amp; ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) &amp; ( not i in Seg k implies e . i = e2 ) ) ) )
proofend;

theorem Th10: :: MATRPROB:10
for D being set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p &amp; len p = n ) )
proofend;

theorem Th11: :: MATRPROB:11
for D being set
for e being FinSequence of D * holds
( ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n iff e is Matrix of D )
proofend;

theorem Th12: :: MATRPROB:12
for i, j being Element of NAT
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( i in Seg (len M) &amp; j in Seg (width M) ) )
proofend;

theorem Th13: :: MATRPROB:13
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M &amp; j in dom (M . i) ) )
proofend;

theorem Th14: :: MATRPROB:14
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j
proofend;

theorem Th15: :: MATRPROB:15
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom (Col (M,j)) &amp; j in dom (Line (M,i)) ) )
proofend;

theorem Th16: :: MATRPROB:16
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i)
proofend;

theorem Th17: :: MATRPROB:17
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
proofend;

theorem Th18: :: MATRPROB:18
for D being non empty set
for m, n being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
proofend;

theorem Th19: :: MATRPROB:19
for D being non empty set
for k being Element of NAT
for m, n being Nat
for e1, e2 being FinSequence of D st len e1 = m &amp; len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) &amp; ( not i in Seg k implies M . i = e2 ) )
proofend;

Lm1:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m &amp; j in dom (m . i) holds
(m . i) . j >= r )
proofend;

Lm2:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m &amp; j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )
proofend;

Lm3:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st j in Seg (width m) &amp; i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
proofend;

definition
let e be FinSequence of REAL * ;
func Sum e ->  FinSequence of REAL  means :Def1: :: MATRPROB:def 1
( len it = len e &amp; ( for k being Element of NAT st k in dom it holds
it . k = Sum (e . k) ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = len e &amp; ( for k being Element of NAT st k in dom b1 holds
b1 . k = Sum (e . k) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = len e &amp; ( for k being Element of NAT st k in dom b1 holds
b1 . k = Sum (e . k) ) &amp; len b2 = len e &amp; ( for k being Element of NAT st k in dom b2 holds
b2 . k = Sum (e . k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Sum MATRPROB:def_1_:_
 for e being FinSequence of REAL *
for b2 being FinSequence of REAL holds
( b2 = Sum e iff ( len b2 = len e &amp; ( for k being Element of NAT st k in dom b2 holds
b2 . k = Sum (e . k) ) ) );

notation
let m be Matrix of REAL;
synonym  LineSum m for  Sum m;
end;

theorem Th20: :: MATRPROB:20
for m being Matrix of REAL holds
( len (Sum m) = len m &amp; ( for i being Element of NAT st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )
proofend;

definition
let m be Matrix of REAL;
func ColSum m ->  FinSequence of REAL  means :Def2: :: MATRPROB:def 2
( len it = width m &amp; ( for j being Nat st j in Seg (width m) holds
it . j = Sum (Col (m,j)) ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = width m &amp; ( for j being Nat st j in Seg (width m) holds
b1 . j = Sum (Col (m,j)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = width m &amp; ( for j being Nat st j in Seg (width m) holds
b1 . j = Sum (Col (m,j)) ) &amp; len b2 = width m &amp; ( for j being Nat st j in Seg (width m) holds
b2 . j = Sum (Col (m,j)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ColSum MATRPROB:def_2_:_
 for m being Matrix of REAL
for b2 being FinSequence of REAL holds
( b2 = ColSum m iff ( len b2 = width m &amp; ( for j being Nat st j in Seg (width m) holds
b2 . j = Sum (Col (m,j)) ) ) );

theorem :: MATRPROB:21
for M being Matrix of REAL st width M > 0 holds
LineSum M = ColSum (M @)
proofend;

theorem Th22: :: MATRPROB:22
for M being Matrix of REAL holds ColSum M = LineSum (M @)
proofend;

definition
let M be Matrix of REAL;
func SumAll M ->  Element of REAL  equals :: MATRPROB:def 3
 Sum (Sum M);
coherence
 Sum (Sum M) is Element of REAL ;
end;

:: deftheorem  defines SumAll MATRPROB:def_3_:_
 for M being Matrix of REAL holds SumAll M = Sum (Sum M);

theorem Th23: :: MATRPROB:23
for M being Matrix of REAL st len M = 0 holds
SumAll M = 0
proofend;

theorem Th24: :: MATRPROB:24
for m being Nat
for M being Matrix of m, 0 , REAL holds SumAll M = 0
proofend;

theorem Th25: :: MATRPROB:25
for k being Element of NAT
for n, m being Nat
for M1 being Matrix of n,k, REAL
for M2 being Matrix of m,k, REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
proofend;

theorem Th26: :: MATRPROB:26
for M1, M2 being Matrix of REAL holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
proofend;

theorem Th27: :: MATRPROB:27
for M1, M2 being Matrix of REAL st len M1 = len M2 holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
proofend;

theorem Th28: :: MATRPROB:28
for M being Matrix of REAL holds SumAll M = SumAll (M @)
proofend;

theorem Th29: :: MATRPROB:29
for M being Matrix of REAL holds SumAll M = Sum (ColSum M)
proofend;

theorem Th30: :: MATRPROB:30
for x, y being FinSequence of REAL st len x = len y holds
len (mlt (x,y)) = len x by FINSEQ_2:72;

theorem Th31: :: MATRPROB:31
for i being Element of NAT
for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R
proofend;

theorem Th32: :: MATRPROB:32
for x being FinSequence of REAL holds mlt (((len x) |-> 1),x) = x
proofend;

theorem Th33: :: MATRPROB:33
for x, y being FinSequence of REAL st ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) &amp; ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) holds
for k being Element of NAT st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0
proofend;

theorem Th34: :: MATRPROB:34
for i being Element of NAT
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 &amp; e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proofend;

theorem Th35: :: MATRPROB:35
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 &amp; e1 = f1 &amp; e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proofend;

theorem Th36: :: MATRPROB:36
for e being FinSequence of REAL
for f being FinSequence of F_Real st e = f holds
Sum e = Sum f
proofend;

notation
let e1, e2 be FinSequence of REAL ;
synonym e1 "*" e2 for |(e1,e2)|;
end;

theorem :: MATRPROB:37
for i being Element of NAT
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 &amp; e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proofend;

theorem Th38: :: MATRPROB:38
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 &amp; e1 = f1 &amp; e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proofend;

theorem Th39: :: MATRPROB:39
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 &amp; width M = width M2 &amp; ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
proofend;

theorem Th40: :: MATRPROB:40
for M being Matrix of REAL
for p being FinSequence of REAL st len M = len p holds
for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))
proofend;

theorem Th41: :: MATRPROB:41
for M being Matrix of REAL
for p being FinSequence of REAL st width M = len p &amp; width M > 0 holds
for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
proofend;

theorem Th42: :: MATRPROB:42
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 &amp; width M = width M2 &amp; ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )
proofend;

definition
let x, y be FinSequence of REAL ;
let M be Matrix of REAL;
assume that
A1: len x = len M and
A2: len y = width M ;
func QuadraticForm (x,M,y) ->  Matrix of REAL means :Def4: :: MATRPROB:def 4
( len it = len x &amp; width it = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) );
existence
 ex b1 being Matrix of REAL st
( len b1 = len x &amp; width b1 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of REAL st len b1 = len x &amp; width b1 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) &amp; len b2 = len x &amp; width b2 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines QuadraticForm MATRPROB:def_4_:_
 for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; len y = width M holds
for b4 being Matrix of REAL holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x &amp; width b4 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) ) );

theorem :: MATRPROB:43
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; len y = width M &amp; len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
proofend;

theorem Th44: :: MATRPROB:44
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; len y = width M &amp; len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
proofend;

theorem :: MATRPROB:45
for x being FinSequence of REAL holds |(x,((len x) |-> 1))| = Sum x by Th32;

theorem Th46: :: MATRPROB:46
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))
proofend;

theorem Th47: :: MATRPROB:47
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; len y = width M &amp; len y > 0 holds
|((x * M),y)| = |(x,(M * y))|
proofend;

theorem :: MATRPROB:48
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M &amp; len x = width M &amp; len x > 0 &amp; len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|
proofend;

theorem Th49: :: MATRPROB:49
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M &amp; len x = width M &amp; len x > 0 &amp; len y > 0 holds
|(x,(y * M))| = |((x * (M @)),y)|
proofend;

theorem Th50: :: MATRPROB:50
for x being FinSequence of REAL
for M being Matrix of REAL st len x = len M &amp; x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
proofend;

theorem :: MATRPROB:51
for x being FinSequence of REAL
for M being Matrix of REAL st len x = width M &amp; width M > 0 &amp; x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))
proofend;

theorem Th52: :: MATRPROB:52
for n being non empty Nat ex P being FinSequence of REAL st
( len P = n &amp; ( for i being Element of NAT st i in dom P holds
P . i >= 0 ) &amp; Sum P = 1 )
proofend;

definition
let p be FinSequence of REAL ;
attrp is ProbFinS  means :Def5: :: MATRPROB:def 5
( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) &amp; Sum p = 1 );
end;

:: deftheorem Def5 defines ProbFinS MATRPROB:def_5_:_
 for p being FinSequence of REAL holds
( p is ProbFinS iff ( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) &amp; Sum p = 1 ) );

registration
cluster non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() ProbFinS for FinSequence of REAL ;
existence
 ex b1 being FinSequence of REAL st
( not b1 is empty &amp; b1 is ProbFinS )
proofend;
end;

theorem :: MATRPROB:53
for p being non empty ProbFinS FinSequence of REAL
for k being Element of NAT st k in dom p holds
p . k <= 1
proofend;

theorem Th54: :: MATRPROB:54
for D being non empty set
for M being non empty-yielding Matrix of D holds
( 1 <= len M &amp; 1 <= width M )
proofend;

definition
let M be Matrix of REAL;
attrM is m-nonnegative  means :Def6: :: MATRPROB:def 6
 for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 ;
end;

:: deftheorem Def6 defines m-nonnegative MATRPROB:def_6_:_
 for M being Matrix of REAL holds
( M is m-nonnegative iff for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 );

definition
let M be Matrix of REAL;
attrM is with_sum=1  means :Def7: :: MATRPROB:def 7
 SumAll M = 1;
end;

:: deftheorem Def7 defines with_sum=1 MATRPROB:def_7_:_
 for M being Matrix of REAL holds
( M is with_sum=1 iff SumAll M = 1 );

definition
let M be Matrix of REAL;
attrM is Joint_Probability  means :Def8: :: MATRPROB:def 8
( M is m-nonnegative &amp; M is with_sum=1 );
end;

:: deftheorem Def8 defines Joint_Probability MATRPROB:def_8_:_
 for M being Matrix of REAL holds
( M is Joint_Probability iff ( M is m-nonnegative &amp; M is with_sum=1 ) );

registration
cluster tabular Joint_Probability  ->  m-nonnegative with_sum=1 for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is Joint_Probability holds
( b1 is m-nonnegative &amp; b1 is with_sum=1 ) by Def8;
cluster tabular m-nonnegative with_sum=1  ->  Joint_Probability for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is m-nonnegative &amp; b1 is with_sum=1 holds
b1 is Joint_Probability by Def8;
end;

theorem Th55: :: MATRPROB:55
for n, m being non empty Nat ex M being Matrix of n,m, REAL st
( M is m-nonnegative &amp; SumAll M = 1 )
proofend;

registration
cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Joint_Probability for FinSequence of REAL * ;
existence
 ex b1 being Matrix of REAL st
( not b1 is empty-yielding &amp; b1 is Joint_Probability )
proofend;
end;

theorem Th56: :: MATRPROB:56
for M being non empty-yielding Joint_Probability Matrix of REAL holds M @ is non empty-yielding Joint_Probability Matrix of REAL
proofend;

theorem :: MATRPROB:57
for M being non empty-yielding Joint_Probability Matrix of REAL
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
proofend;

definition
let M be Matrix of REAL;
attrM is with_line_sum=1  means :Def9: :: MATRPROB:def 9
 for k being Element of NAT st k in dom M holds
Sum (M . k) = 1;
end;

:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def_9_:_
 for M being Matrix of REAL holds
( M is with_line_sum=1 iff for k being Element of NAT st k in dom M holds
Sum (M . k) = 1 );

theorem Th58: :: MATRPROB:58
for n, m being non empty Nat ex M being Matrix of n,m, REAL st
( M is m-nonnegative &amp; M is with_line_sum=1 )
proofend;

definition
let M be Matrix of REAL;
attrM is Conditional_Probability  means :Def10: :: MATRPROB:def 10
( M is m-nonnegative &amp; M is with_line_sum=1 );
end;

:: deftheorem Def10 defines Conditional_Probability MATRPROB:def_10_:_
 for M being Matrix of REAL holds
( M is Conditional_Probability iff ( M is m-nonnegative &amp; M is with_line_sum=1 ) );

registration
cluster tabular Conditional_Probability  ->  m-nonnegative with_line_sum=1 for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is Conditional_Probability holds
( b1 is m-nonnegative &amp; b1 is with_line_sum=1 ) by Def10;
cluster tabular m-nonnegative with_line_sum=1  ->  Conditional_Probability for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is m-nonnegative &amp; b1 is with_line_sum=1 holds
b1 is Conditional_Probability by Def10;
end;

registration
cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Conditional_Probability for FinSequence of REAL * ;
existence
 ex b1 being Matrix of REAL st
( not b1 is empty-yielding &amp; b1 is Conditional_Probability )
proofend;
end;

theorem :: MATRPROB:59
for M being non empty-yielding Conditional_Probability Matrix of REAL
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
proofend;

theorem Th60: :: MATRPROB:60
for M being non empty-yielding Matrix of REAL holds
( M is non empty-yielding Conditional_Probability Matrix of REAL iff for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )
proofend;

theorem :: MATRPROB:61
for M being non empty-yielding with_line_sum=1 Matrix of REAL holds SumAll M = len M
proofend;

notation
let M be Matrix of REAL;
synonym  Row_Marginal M for  LineSum M;
synonym  Column_Marginal M for  ColSum M;
end;

registration
let M be non empty-yielding Joint_Probability Matrix of REAL;
cluster Sum M ->  non empty ProbFinS ;
coherence
 ( not Row_Marginal M is empty &amp; Row_Marginal M is ProbFinS )
proofend;
cluster ColSum M ->  non empty ProbFinS ;
coherence
 ( not Column_Marginal M is empty &amp; Column_Marginal M is ProbFinS )
proofend;
end;

registration
let M be non empty-yielding Matrix of REAL;
clusterM @  ->  non empty-yielding ;
coherence
 not M @ is empty-yielding
proofend;
end;

registration
let M be non empty-yielding Joint_Probability Matrix of REAL;
clusterM @  ->  Joint_Probability ;
coherence
 M @ is Joint_Probability by Th56;
end;

theorem Th62: :: MATRPROB:62
for p being non empty ProbFinS FinSequence of REAL
for P being non empty-yielding Conditional_Probability Matrix of REAL st len p = len P holds
( p * P is non empty ProbFinS FinSequence of REAL &amp; len (p * P) = width P )
proofend;

theorem :: MATRPROB:63
for P1, P2 being non empty-yielding Conditional_Probability Matrix of REAL st width P1 = len P2 holds
( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL &amp; len (P1 * P2) = len P1 &amp; width (P1 * P2) = width P2 )
proofend;