for p, q being ProbFinS FinSequence of REAL holds Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS by Th23, Th44;