reconsider n = n as Element of NAT by ORDINAL1:def 13;
(n |-> 0 ) +* i,1 = Replace (n |-> 0 ),i,1 ;
hence (n |-> 0 ) +* i,1 is FinSequence of REAL ; :: thesis: verum