How to justify that $\neg A \vee A$ has a sense? We do substitutions from the set of axioms that we have to prove some statement.
I can't understand what actions we should do to go from (1) to (2). What kind of substitution should be made?
The screenshot is from Opera Magistris v4 page 143 https://archive.org/details/OperaMagistris/page/n143/mode/2up?view=theater

 A: Huh!  This is a (horribly!) defective proof.
First, we know it is defective, since line 2 is not a logical truth (tautology), and in this system we only prove logical truths, meaning that every line need to be a logical truth by itself.
I am pretty sure that the author meant line 2 to be $A \to (A \lor A)$. Indeed, that statement would be the result of substituting the formula $A$ for the letter $B$ in line 1.
But, this is not the only thing that is going wrong in this proof:
The author lists 7 and A1 as the justification for line 8, but I am not exactly sure how the author intends to accomplish that. I think that the author thinks that given that A1 says that $(A \lor A)$ implies $A$, the author seems to want to use this to replace $A \lor A$ with $A$ in line 7.  However, there is no rule that allows you to do such a thing, and in fact, that could easily lead to invalid inferences! For example, just because $A$ implies $B$ does not mean that $A \to C$ implies $A \to C$.
Third, the author claims that PA5 is Axiom 5 from Russell and Whitehead, but it is not that at all. In fact, the A5 listed here is not even a logical truth! The right axiom is:
$$PM5.  (B \to C) \to ((A \lor B) \to (A \lor C))$$
but that brings me to:
Fourth: line 3 is neither an instance of the defective A5, nor of PM5.
Instead, line 4 is an instance of PM5.... but I see no way it can be obtained from line 3
Fifth, the author says that line 9 is obtained through Modus Ponens on line 8, but Modus Ponens requires a second line, which the author does not indicate. However, that other line would either have to be $A \to A$, or $((A \to A) \to (A \to A)) \to (A \to A)$, neither of which occur earlier in the proof.  What would make sense, is to do a Modus Ponens on A1 and line 7.
So .. here is what a proper proof would have looked like:

*

*$A \to (A \lor A) \  \text{(instance of A2)}$

*$((A \lor A) \to A) \to ((\neg A \lor (A \lor A)) \to (\neg A \lor A)) \text{(instance of PM5)}$

*$((A \lor A) \to A) \to ((A \to (A \lor A)) \to (A \to A)) \text{(3 and property of $\to$)}$

*$(A \lor A) \to A \  \text{(instance of A1)}$

*$(A \to (A \lor A)) \to (A \to A) \text{(3 and 4, Modus Ponens)}$

*$A \to A \text{(1 and 5, Modus Ponens)}$

*$\neg A \lor A \text{(6 and property of $\to$)}$
I think this is what the author intended to do, but it ends up looking nothing like it.  What a mess!! Please stop using this source!!
A: As per the answer above, Ax.5 is simply wrong.
Using the correct one, with the substitution: $\lnot A$ in place of $A$, we have:

*

*$(B→C) → ((\lnot A∨B)→(\lnot A∨C))$,

that is equivalent [by the definition of $\to$] to:


*$(B \to C) → ((A \to B)→(A \to C))$.

Applying the substitution: $A \lor A$ in place of $B$; $A$ in place of $C$, we get:


*$((A \lor A) \to A) \to [(A \to (A \lor A))\to (A \to A)]$.

Using Ax.1 and Modus Ponens, we get:


*$(A \to (A \lor A))\to (A \to A)$.

Using Ax.2 [with the substitution: $A$ in place of $B$] and MP we get:


*$A \to A$.

Finally, we have to rewrite is using the def. of $\to$ to get:

$\lnot A \lor A$.

