List of theorems referencing the symbol FIN_SEQS
(369) Theorem 318: [Finite sequences are single_valued maps with integer domains] (F in Fin_seqs(S)) •eq (Svm(F) & (domain(F) in Za) & (range(F) •incin S))
(370) Theorem 319: [Other properties of finite sequences] (F in Fin_seqs(S)) •imp ((domain(F) = #domain(F)) & (domain(F) = #F) & (#F in Za) & Finite(F))
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(381) Theorem 330: [Concatenation of finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp ((concat(F,G) in Fin_seqs(S)) & (domain(concat(F,G)) = domain(F) •PLUS domain(G)) & (range(concat(F,G)) = range(F) + range(G))) & ((U in domain(F) •PLUS domain(G)) •imp (concat(F,G)~[U] = if U in domain(F) then F~[U] else G~[U •MINUS domain(F)] end if))
(382) Theorem 331: [0 is bilateral unit for sequence concatenation] (F in Fin_seqs(S)) •imp ((concat(F,0) = F) & (concat(0,F) = F))
(383) Theorem 332: [Associativity of sequence concatenation] ((F in Fin_seqs(S)) & (G in Fin_seqs(S)) & (H in Fin_seqs(S))) •imp (concat(F,concat(G,H)) = concat(concat(F,G),H))
(384) Theorem 333: [Concatenation of shifted sequences] ((F in Fin_seqs(S)) & (M in domain(F))) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (F = concat((F •ON M), shifted_seq(F,M))))
(389) Theorem 334: ((F in Fin_seqs(S)) & (G in Subseqs(F))) •imp ((G in Fin_seqs(S)) & (domain(G) in next(domain(F))))
(391) Theorem 336: ((F in Fin_seqs(S)) & (M in Za)) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) in next(domain(F))))
(902) Theorem 747: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re)) & (X in Re)) •imp (((Polval(F,X) •R_PLUS Polval(G,X)) = Polval(F •PolPlus G,X)) & ((Polval(F,X) •R_MINUS Polval(G,X)) = Polval(F •PolMinus G,X)) & ((Polval(F,X) •R_TIMES Polval(G,X)) = Polval(F •PolTimes G,X)))
(903) Theorem 748: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp (((PolFcn(F) •F_PLUS PolFcn(G)) = PolFcn(F •PolPlus G)) & ((PolFcn(F) •F_MINUS PolFcn(G)) = PolFcn(F •PolMinus G)) & ((PolFcn(F) •F_TIMES PolFcn(G)) = PolFcn(F •PolTimes G)))
(908) Theorem 753: [Polynomial functions are continuous everywhere] (F in Fin_Seqs(Re)) •imp Cf_RR(PolFcn(F),Re)
(909) Theorem 754: [Polynomial quotients are continuous wherever their denominator is nonzero] ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp Cf_RR(F •F_OVER G,{x in Re | G~[x] /= R_0})