reconsider n = n as Nat ;
(n |-> 0) +* (i,1) = Replace ((n |-> (In (0,REAL))),i,(In (1,REAL))) ;
hence (n |-> 0) +* (i,1) is FinSequence of REAL ; :: thesis: verum