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