I don't want to make this to general because I think I would make a mistake then but I think one can generalize this idea for every uniqueness/injectivity proof:
The claim is:
$V$ vector space over $F\wedge B$ basis of $V$ $\Rightarrow\forall v\in V\exists !(B_v,c):B_v\subseteq B\wedge B_v \text{ finite } \wedge c:B_v\rightarrow F\backslash\{0\}\wedge v=\sum_{b\in B_v}c(b)b$
My first question is what is the actual logical definition of $\exists!$ ?
To prove the uniqueness I think we have to show the implication
$\exists(B_v,c),(\bar{B_v},\bar{c}):B_v\subseteq B\wedge B_v \text{ finite } \wedge c:B_v\rightarrow F\backslash\{0\}\wedge \bar{B_v}\subseteq B\wedge \bar{B}_v \text{ finite } \wedge \bar{c}:\bar{B_v}\rightarrow F\backslash\{0\}\wedge \big((B_v,c)=(\bar{B_v},\bar{c})\vee (B_v,c)\neq(\bar{B_v},\bar{c})\big)\wedge v=\sum_{b\in B_v}c(b)b=\sum_{b\in \bar{B}_v}\bar{c}(b)b\Rightarrow (B_v,c)=(\bar{B_v},\bar{c})$
But I don't know how we would transcribe this statement to English because in my head I think about:
If we have two pairs that are in the solutionset (i.e that fulfill desired qualities) and the pairs might be different or equal then the pairs are equal
The problem I have here is that if I say two pairs then I automatically think about two different pairs. So how can we reformulate the statement, i.e. what are we proving here in English? How can I express it?
$\exists !$ means "There is exactly one", so that expresses uniqueness right there.
Without using $\exists !$, you can use several strategies:
First, we can express that there is one .. and no other one. So, you would get something like:
$\exists c (bla \ bla \ bla (c) \land \neg \exists c' (c' \not = c \land bla \ bla \ bla(c')))$
We can also say that there is one with the property, and everything that has the property must equal that first one:
$\exists c (bla \ bla \ bla (c) \land \forall c' ( bla \ bla \ bla(c') \to c' = c))$
Finally, we can use this structure:
$\exists c \forall c' (bla \ bla \ bla (c') \leftrightarrow c' = c))$
See how this last one works? When $c' =c$, the right side holds true, and hence we must have $bla \ bla \ bla (c')$, and since $c'=c$ we thus have $bla \ bla \ bla (c)$. And for any $c' \not = c$, the right side is false, and ehnce the left side should be false too, and hence we have $\neg bla \ bla \ bla (c')$ for any $c' \not = c$