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