Is infinite-length formula allowed in ZFC? I am curious whether infinite-length formulas are allowed in ZFC. If it is not, then how does it express the case where infinite number of terms (in ordinary mathematics) are being handled? (Like proving that limit of sum of numbers in a sequence is a particular number and so on) (Well, one may say that for limit, that can be done by specifying a formula for sequence, but there are cases where this might not be the case.)
Another way of viewing this problem: can a function or predicate be defined with infinite number of variables (both free and bound)?
For example, given a set of sequences of infinite cardinality (so the number of sequences in the set is infinite), a function takes out nth number from each sequence to form a set (so this function would take one set and map to set)- would this be a valid function in zfc?
 A: I am going to assume that you mean "formula" in the logical meaning of the word. Formulas do not live "within $\sf ZFC$", but rather in the logic outside it, which is first-order logic and therefore does not permit infinitary formulas.
However, internally to $\sf ZFC$ we can define first-order logic, and we can define stronger logics, such as infinitary logics $\mathcal L_{\kappa,\lambda}$ which allow conjunction and disjunction of $<\kappa$ formulas, and $<\lambda$ quantifiers.
But we don't really need that for just simple things, that you might have had in mind, we can talk about functions whose domain is a function from an infinite set into the domain. For example, an $\omega$-tuple is just a function from $\omega$ into $X$. So a function taking $\omega$ variables is really a function taking as input a function from $\omega$ into $X$.
This can be extended in several different ways, but as with everything else in mathematics, once you allow infinite objects into your system, you add difficulties and some cases require more attentive and careful considerations.
A: In ZFC, sequences are represented by functions over $\mathbb{N}$. And functions, in turn, are represented by sets of pairs mapping an element of to domain to an element of the codomain. Thus, a sequence in ZFC corresponds to a set $\{(0,a_0),(1,a_1),\ldots\}$, where pairs $(a,b)$ stand for the set $\{a,\{a,b\}\}$. A set can thus represent a whole sequence, so infinit formulas aren't required to talk about infinite sets.
The ZFC axioms are usually formalized in first-order predicate logic, which does not permit infinit formulas. In principle, you could take the axioms of ZFC, and use some kind of infinitary logic. But for these logics, the compactness and completeness theorems fail, so you'd have to tread very carefully. These theorems guarantee that sentences are semantically true (i.e., true in all models) exactly if they are provable, and that theories are semantically consistent (i.e., have a model) exactly if they prove no contradiction. These aren't properties that one would give up lightly.
