let p, q be ProbFinS FinSequence of REAL ; :: thesis: Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS
(ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability Matrix of REAL by Th23;
hence Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS by Th44; :: thesis: verum