:: 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-2011 Association of Mizar Users

begin

definition

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

proof end;

end;

definition

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

proof end;

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 & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )

proof end;

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 & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )

proof end;

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 & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m

proof end;

theorem Th4: :: MATRPROB:4

for e being FinSequence of REAL st len e >= 1 & ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st f . 1 = e . 1 & ( for n being Nat st 0 <> n & 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

proof end;

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

proof end;

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 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )

proof end;

theorem Th7: :: MATRPROB:7

for F being FinSequence of REAL ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )

proof end;

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 *

proof end;

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 & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )

proof end;

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 & len p = n ) )

proof end;

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 )

proof end;

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) & j in Seg (width M) ) )

proof end;

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 & j in dom (M . i) ) )

proof end;

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

proof end;

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)) & j in dom (Line (M,i)) ) )

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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 & 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 ) & ( not i in Seg k implies M . i = e2 ) )

proof end;

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 & j in dom (m . i) holds
(m . i) . j >= r )

proof end;

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 & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )

proof end;

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) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )

proof end;

definition

let e be FinSequence of REAL * ;
func Sum e -> FinSequence of REAL means :Def1: :: MATRPROB:def 1
( len it = len e & ( for k being Element of NAT st k in dom it holds
it . k = Sum (e . k) ) );
existence
ex b₁ being FinSequence of REAL st
( len b₁ = len e & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = Sum (e . k) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len e & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = Sum (e . k) ) & len b₂ = len e & ( for k being Element of NAT st k in dom b₂ holds
b₂ . k = Sum (e . k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Sum MATRPROB:def 1 :
for e being FinSequence of REAL *
for b₂ being FinSequence of REAL holds
( b₂ = Sum e iff ( len b₂ = len e & ( for k being Element of NAT st k in dom b₂ holds
b₂ . 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 & ( for i being Element of NAT st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )

proof end;

definition

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

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = width m & ( for j being Nat st j in Seg (width m) holds
b₁ . j = Sum (Col (m,j)) ) & len b₂ = width m & ( for j being Nat st j in Seg (width m) holds
b₂ . j = Sum (Col (m,j)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ColSum MATRPROB:def 2 :
for m being Matrix of REAL
for b₂ being FinSequence of REAL holds
( b₂ = ColSum m iff ( len b₂ = width m & ( for j being Nat st j in Seg (width m) holds
b₂ . j = Sum (Col (m,j)) ) ) );

theorem :: MATRPROB:21

for M being Matrix of REAL st width M > 0 holds
LineSum M = ColSum (M @)

proof end;

theorem Th22: :: MATRPROB:22

for M being Matrix of REAL holds ColSum M = LineSum (M @)

proof end;

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

proof end;

theorem Th24: :: MATRPROB:24

for m being Nat
for M being Matrix of m, 0 , REAL holds SumAll M = 0

proof end;

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)

proof end;

theorem Th26: :: MATRPROB:26

for M1, M2 being Matrix of REAL holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

proof end;

theorem Th27: :: MATRPROB:27

for M1, M2 being Matrix of REAL st len M1 = len M2 holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)

proof end;

theorem Th28: :: MATRPROB:28

for M being Matrix of REAL holds SumAll M = SumAll (M @)

proof end;

theorem Th29: :: MATRPROB:29

for M being Matrix of REAL holds SumAll M = Sum (ColSum M)

proof end;

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:86;

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

proof end;

theorem Th32: :: MATRPROB:32

for x being FinSequence of REAL holds mlt (((len x) |-> 1),x) = x

proof end;

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 ) & ( 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

proof end;

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 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)

proof end;

theorem Th35: :: MATRPROB:35

for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)

proof end;

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

proof end;

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 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2

proof end;

theorem Th38: :: MATRPROB:38

for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2

proof end;

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 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )

proof end;

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))

proof end;

theorem Th41: :: MATRPROB:41

for M being Matrix of REAL
for p being FinSequence of REAL st width M = len p & 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

proof end;

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 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )

proof end;

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 & width it = len y & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) );
existence
ex b₁ being Matrix of REAL st
( len b₁ = len x & width b₁ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st len b₁ = len x & width b₁ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) & len b₂ = len x & width b₂ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) holds
b₁ = b₂

proof end;

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 & len y = width M holds
for b₄ being Matrix of REAL holds
( b₄ = QuadraticForm (x,M,y) iff ( len b₄ = len x & width b₄ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₄ * (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 & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)

proof end;

theorem Th44: :: MATRPROB:44

for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))

proof end;

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 & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))

proof end;

theorem Th47: :: MATRPROB:47

for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|((x * M),y)| = |(x,(M * y))|

proof end;

theorem :: MATRPROB:48

for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|

proof end;

theorem Th49: :: MATRPROB:49

for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|(x,(y * M))| = |((x * (M @)),y)|

proof end;

theorem Th50: :: MATRPROB:50

for x being FinSequence of REAL
for M being Matrix of REAL st len x = len M & 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))

proof end;

theorem :: MATRPROB:51

for x being FinSequence of REAL
for M being Matrix of REAL st len x = width M & width M > 0 & 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))

proof end;

theorem Th52: :: MATRPROB:52

for n being non empty Nat ex P being FinSequence of REAL st
( len P = n & ( for i being Element of NAT st i in dom P holds
P . i >= 0 ) & Sum P = 1 )

proof end;

definition

let p be FinSequence of REAL ;
attr p is ProbFinS means :Def5: :: MATRPROB:def 5
( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) & 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 ) & Sum p = 1 ) );

registration

cluster non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V149() V150() ProbFinS FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st
( not b₁ is empty & b₁ is ProbFinS )

proof end;

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

proof end;

theorem Th54: :: MATRPROB:54

for D being non empty set
for M being non empty-yielding Matrix of D holds
( 1 <= len M & 1 <= width M )

proof end;

definition

let M be Matrix of REAL;
attr M 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;
attr M 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;
attr M is Joint_Probability means :Def8: :: MATRPROB:def 8
( M is m-nonnegative & 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 & M is with_sum=1 ) );

registration

cluster tabular Joint_Probability -> m-nonnegative with_sum=1 FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is Joint_Probability holds
( b₁ is m-nonnegative & b₁ is with_sum=1 ) by Def8;
cluster tabular m-nonnegative with_sum=1 -> Joint_Probability FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is m-nonnegative & b₁ is with_sum=1 holds
b₁ 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 & SumAll M = 1 )

proof end;

registration

cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V173() Joint_Probability FinSequence of REAL * ;
existence
ex b₁ being Matrix of REAL st
( not b₁ is empty-yielding & b₁ is Joint_Probability )

proof end;

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

proof end;

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

proof end;

definition

let M be Matrix of REAL;
attr M 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 & M is with_line_sum=1 )

proof end;

definition

let M be Matrix of REAL;
attr M is Conditional_Probability means :Def10: :: MATRPROB:def 10
( M is m-nonnegative & 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 & M is with_line_sum=1 ) );

registration

cluster tabular Conditional_Probability -> m-nonnegative with_line_sum=1 FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is Conditional_Probability holds
( b₁ is m-nonnegative & b₁ is with_line_sum=1 ) by Def10;
cluster tabular m-nonnegative with_line_sum=1 -> Conditional_Probability FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is m-nonnegative & b₁ is with_line_sum=1 holds
b₁ 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 V173() Conditional_Probability FinSequence of REAL * ;
existence
ex b₁ being Matrix of REAL st
( not b₁ is empty-yielding & b₁ is Conditional_Probability )

proof end;

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

proof end;

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 )

proof end;

theorem :: MATRPROB:61

for M being non empty-yielding with_line_sum=1 Matrix of REAL holds SumAll M = len M

proof end;

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 & Row_Marginal M is ProbFinS )

proof end;

cluster ColSum M -> non empty ProbFinS ;
coherence
( not Column_Marginal M is empty & Column_Marginal M is ProbFinS )

proof end;

end;

registration

let M be non empty-yielding Matrix of REAL;
cluster M @ -> non empty-yielding ;
coherence
not M @ is empty-yielding

proof end;

end;

registration

let M be non empty-yielding Joint_Probability Matrix of REAL;
cluster M @ -> 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 & len (p * P) = width P )

proof end;

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 & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )

proof end;