n |-> jj is Element of REAL n ;
hence 1* n is Element of REAL n ; :: thesis: verum