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?