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