reconsider VAR' = VAR as non empty Subset of NAT ;
reconsider x' = x as Element of VAR' ;
reconsider x' = x' as Element of NAT ;
<*x'*> is FinSequence of NAT ;
hence <*x*> is FinSequence of NAT ; :: thesis: verum