IT . x is Element of REAL n ;
hence IT . x is Element of REAL n ; :: thesis: verum