I don't know about the OSA system specifically. However, here's a proof that I wrote up in Coq using types. Most of the length of this is just the setup, then the actual proof becomes very short.
Parameters Horse Dog Greyhound Rabbit Animal : Type.
Parameter Horse_inc_Animal : Horse -> Animal.
Parameter Dog_inc_Animal : Dog -> Animal.
Parameter Greyhound_inc_Dog : Greyhound -> Dog. (* 3a *)
Parameter Rabbit_inc_Animal : Rabbit -> Animal.
Coercion Horse_inc_Animal : Horse >-> Animal.
Coercion Dog_inc_Animal : Dog >-> Animal.
Coercion Greyhound_inc_Dog : Greyhound >-> Dog.
Coercion Rabbit_inc_Animal : Rabbit >-> Animal.
Parameter Faster : Animal -> Animal -> Prop.
Axiom stmt_1a : forall (x : Horse) (y : Dog),
Faster x y.
Axiom stmt_2a : exists y : Greyhound,
forall z : Rabbit, Faster y z.
Axiom stmt_4a : forall x y z : Animal,
Faster x y -> Faster y z -> Faster x z.
Parameter Harry : Horse. (* 5a *)
Parameter Ralph : Rabbit. (* 6a *)
(* Main result... *)
Goal Faster Harry Ralph.
Proof.
(* existential elimination on (2a) *)
destruct stmt_2a as [g].
(* specialization of (4a), and also implicitly applies ->E (modus ponens)
a couple of times *)
apply stmt_4a with (y := g).
(* Subgoal: Faster Harry g,
proved by specializing (1a) *)
+ apply stmt_1a.
(* Subgoal: Faster g Ralph,
proved by specializing the statement
H : forall z : Rabbit, faster g z
gotten from the existential elimination *)
+ apply H.
Qed.
Again, I don't know how much this would help in constructing a proof in your particular system - I'm just posting in the hopes that it might be close enough to be of some help. (Do keep in mind that Coq is often oriented towards top-down programming of a proof, as in this case, whereas Fitch-style systems are often closer to bottom-up serializations of the same proof term.)
Two-sorted logic is not an "informal short-cut", it is actually a different way of setting up formal logic. In particular, the two different kinds of variables actually matter to the semantics.
So, if you set up Morse-Kelly set theory as a two-sorted theory, then a model is not just a set $M$ together with a relation $\in$ but rather a tuple $(M,S,C,\in)$ where $M$ is a set, $S$ and $C$ are subsets of $M$ (the sets and classes) whose union is $M$, and $\in$ is a binary relation on $M$. When we interpret formulas in such a structure, the set variables get interpreted as elements of $S$ and the class variables as elments of $C$. In other words, if $x$ is a set variable, then $M\models\forall x[\varphi(x)]$ is defined as $\forall a\in S, M\models \varphi(a)$, and similarly for class variables and existential quantifiers. Similarly, if you're studying proofs, then every variable has a sort and all the deduction rules need to respect these sorts, so for instance when you use universal instantiation you are only allowed to replace the quantified variable with another variable of the same sort. As a result, proofs will be sound with respect to this semantics.
Now a warning: the setup above is not quite the usual definition of multisorted logic. Usually in multisorted logic, the sets for different sorts are required to be disjoint (so $S$ and $C$ would be disjoint), and all the function and relation symbols must specify (as part of their "arity") the sorts of their inputs (and output, for functions). So for instance, to talk about something like modules over a ring, you would have a language with two sorts $R$ (the ring) and $M$ (the module), and for each of the different function symbols you would specify their input and output; for instance, there would be both an addition function $+_R$ which takes two inputs in $R$ and gives an output in $R$ and an addition function $+_M$ which takes two inputs in $M$ and gives an output in $M$, and there would be a scalar multiplication function $\cdot_M$ which takes an input in $R$ and an input in $M$ and gives an output in $M$. A model would then be a tuple $(X,R,M,+_R,+_M,\cdot_M,\dots)$ (there are a few more functions needed which I've omitted) where $R$ and $M$ are disjoint sets whose union is $X$, $+_R$ is a function $R\times R\to R$, $+_M$ is a function $M\times M\to M$, and so on. Moreover, in this language, not only does each variable have a type, but each term has a type: for instance, if $r$ and $s$ are $R$-variables, then $+_R(r,s)$ is an $R$-term, but $+_M(r,s)$ is not a well-formed term at all since we can't input $R$-variables into $+_M$.
This usual definition doesn't work so well for Morse-Kelly because we'd like to be able to talk about sets being equal to classes, and sets being elements of both sets and classes. To use disjoint types, in a model we would need to have, for each set, a "copy" of the set which is a class with the same elements but is not literally equal. We would also need to have two different element relations $\in_S$ and $\in_C$, where $\in_S$ is a relation between two sets and $\in_C$ is a relation between a set and a class. We couldn't actually talk about sets and classes being equal (since they never are!), and to say something like $\forall x \exists X (x = X)$ we would need to say that $x=X$ is actually just an abbreviation for $\forall y(y\in_S x\Leftrightarrow y\in_C X)$.
Best Answer
Rob Arthan's answer is correct, but it has the downside that if $T$ is a many-sorted theory and $T'$ is the corresponding single-sorted theory, then $T$ and $T'$ fail to be bi-interpretable (since the "junk" interpretations of the functions symbols outside of their intended domains cannot be recovered after passing from a model of $T'$ to a model of $T$).
An alternative is simply to replace every function symbol with a relation symbol defining its graph. So for example replace scalar multiplication with a ternary relation symbol $R$ and add the axioms $$\forall x\forall y\forall z\,(R(x,y,z)\to P_F(x)\land P_V(y)\land P_V(z))$$ and $$\forall x\forall y\,(P_F(x)\land P_V(y)\to \exists^! z\, R(x,y,z)).$$ Following this approach, we can find a single-sorted $T'$ which is actually bi-interpretable with $T$.