take the n -element XFinSequence of REAL ; :: thesis: ( the n -element XFinSequence of REAL is n -element & the n -element XFinSequence of REAL is real-valued )
thus ( the n -element XFinSequence of REAL is n -element & the n -element XFinSequence of REAL is real-valued ) ; :: thesis: verum