let p be non empty ProbFinS FinSequence of REAL ; for P being V3() 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 )
set n = len p;
let P be V3() Conditional_Probability Matrix of REAL; ( len p = len P implies ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P ) )
assume A1:
len p = len P
; ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
A2:
len (p * P) = width P
by A1, MATRIXR1:62;
A3:
for i being Nat st i in dom (p * P) holds
(p * P) . i >= 0
proof
let i be
Nat;
( i in dom (p * P) implies (p * P) . i >= 0 )
assume A4:
i in dom (p * P)
;
(p * P) . i >= 0
i in Seg (len (p * P))
by A4, FINSEQ_1:def 3;
then A5:
(p * P) . i =
p "*" (Col (P,i))
by A1, Th40
.=
Sum (mlt (p,(Col (P,i))))
;
A6:
for
i,
j being
Nat st
[i,j] in Indices P holds
P * (
i,
j)
>= 0
by Def6;
i in Seg (width P)
by A2, A4, FINSEQ_1:def 3;
then A7:
for
j being
Nat st
j in dom (Col (P,i)) holds
(Col (P,i)) . j >= 0
by A6, Lm3;
for
i being
Nat st
i in dom p holds
p . i >= 0
by Def5;
then
for
k being
Nat st
k in dom (mlt (p,(Col (P,i)))) holds
(mlt (p,(Col (P,i)))) . k >= 0
by A7, Th33;
hence
(p * P) . i >= 0
by A5, RVSUM_1:84;
verum
end;
set m = width P;
set e = (width P) |-> jj;
A8:
len ((width P) |-> jj) = width P
by CARD_1:def 7;
A9:
width P > 0
by Th54;
then A10:
len (P @) = width P
by MATRIX_0:54;
width (P @) = len P
by A9, MATRIX_0:54;
then A11:
len (((width P) |-> jj) * (P @)) = len p
by A1, A8, A10, MATRIXR1:62;
for k being Nat st k in dom (((width P) |-> jj) * (P @)) holds
(((width P) |-> jj) * (P @)) . k = 1
proof
let k be
Nat;
( k in dom (((width P) |-> jj) * (P @)) implies (((width P) |-> jj) * (P @)) . k = 1 )
assume
k in dom (((width P) |-> jj) * (P @))
;
(((width P) |-> jj) * (P @)) . k = 1
then A12:
k in Seg (len (((width P) |-> jj) * (P @)))
by FINSEQ_1:def 3;
then A13:
k in dom P
by A1, A11, FINSEQ_1:def 3;
thus (((width P) |-> jj) * (P @)) . k =
Sum (Col ((P @),k))
by A8, A10, A12, Th50
.=
Sum (Line (P,k))
by A13, MATRIX_0:58
.=
Sum (P . k)
by A13, MATRIX_0:60
.=
1
by A13, Def9
;
verum
end;
then A14:
((width P) |-> jj) * (P @) = (len p) |-> jj
by A11, Th1;
Sum (p * P) =
|((p * P),((width P) |-> jj))|
by A2, Th32
.=
|(p,(((width P) |-> jj) * (P @)))|
by A1, A9, A8, Th49
.=
Sum p
by A14, Th32
.=
1
by Def5
;
hence
( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
by A2, A3, Def5, Th54; verum