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