take the non empty ProbFinS FinSequence of REAL ; :: thesis: ( not the non empty ProbFinS FinSequence of REAL is empty & the non empty ProbFinS FinSequence of REAL is ProbFinS )
thus ( not the non empty ProbFinS FinSequence of REAL is empty & the non empty ProbFinS FinSequence of REAL is ProbFinS ) ; :: thesis: verum