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

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