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