CF7. Let $\boldsymbol{A}$ be a relation (resp. a term) in a theory $\mathcal{T}$, and let $\boldsymbol{x}$ and $\boldsymbol{y}$ be letters. Then $(\boldsymbol{y}|\boldsymbol{x})\boldsymbol{A}$ is a relation (resp. a term) in $\mathcal{T}$.
Is this supposed to be understood as one theorem formulated as follows: if $\boldsymbol{A}$ is a relation, then $(\boldsymbol{y}|\boldsymbol{x})\boldsymbol{A}$ is a relation and if $\boldsymbol{A}$ is a term, then $(\boldsymbol{y}|\boldsymbol{x})\boldsymbol{A}$ is a term? Judging by what the authors wrote in (a)
and we know already that $\boldsymbol{A'_j}$ is a relation
the inductive step is the following statement:
if $\boldsymbol{A_k}$ is a relation, then $\boldsymbol{A'_k}$ is a relation for and if $\boldsymbol{A_k}$ is a term, then $\boldsymbol{A'_k}$ is a term for $k=1,2,...,i-1$
Am I right? Maybe we should prove it as two different theorems with two respective inductive hypotheses? Why can we join them together in one theorem?
Question 1:
That is correct. In Chapter 1 / 1.Terms and Relations / 1.Signs and Assemblies you can read the following:
So, if A is a relation and contains the letter x, you are replacing the letter x with another letter y. This will not change the fact, that A is still a relation.
On page 22 below CF7 you can read "If Ai is preceded in the construction by a relation Aj, such that Ai is not(Aj), then Ai' is identical to with not(Aj') by CS5 (which is (C|x)(not(A)) is identical with not(A')), and not(Aj') is a relation by CF2." Following this trace backwards, "we know already that Aj' is a relation."
I'm also working my way through Bourbaki, so this is how I get it.