Theorem: State on Unital C*-Subalgebra extends to whole C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra. 
Let $B$ be a unital $\text C^\ast$-subalgebra of $A$.
Let $f_1 : B \to \C$ be a state.
Then there exists a state $f : A \to \C$ extending $f_1$.

Proof:
Let $\le_A$ be the canonical preordering of $A$.
Let $B_{\mathbf {SA} }$ and $A_{\mathbf {SA} }$ be the set of Hermitian elements of $B$ and $A$ respectively.
From Hermitian Elements of *-Algebra form Real Vector Subspace, these are vector spaces over $\R$. 
From Bounds on Hermitian Element of Unital C*-Algebra in terms of Bounds on Spectrum, for each $a \in A_{\mathbf {SA} }$ we have:
:$a \le_A \norm a {\mathbf 1}_A$
where $\norm a {\mathbf 1}_A \in B_{\mathbf {SA} }$. 
Hence $B_{\mathbf {SA} }$ is cofinal in the preordered vector space $\struct {A_{\mathbf {SA} }, \le_A}$.
From Positive Linear Functional on C*-Algebra preserves Star and Complex Number equals Conjugate iff Wholly Real, $f_1$ is real-valued on $B_{\mathbf {SA} }$. 
Hence from Extension Theorem for Positive Linear Functional defined on Cofinal Linear Subspace, there exists a positive linear functional $f_0 : A_{\mathbf {SA} } \to \R$ extending $f_1 \restriction {B_{\mathbf {SA} } }$.
For general $a \in A$, define:
:$\map f a = \map {f_0} {\map \Re a} + i \map {f_0} {\map \Im a}$
For $b \in B$, we have: 
{{begin-eqn}}
{{eqn	| l = \map f b
		| r = \map {f_0} {\map \Re b} + i \map {f_0} {\map \Im b} 
}}
{{eqn	| r = \map {f_1} {\map \Re b} + i \map {f_1} {\map \Im b}
		| c = $f_0 \restriction B_{\mathbf{SA} } = f_1 \restriction B_{\mathbf{SA} }$
}}
{{eqn	| r = \map {f_1} {\map \Re b + i \map \Im b} 
		| c = $f_1$ is linear
}}
{{eqn	| r = \map {f_1} b 
		| c = Element of *-Algebra Uniquely Decomposes into Hermitian Elements
}}
{{end-eqn}}
Hence $f$ extends $f_1$. 
We show that $f$ is as desired.
We first show that $f$ is linear.
Firstly, for $a \in A$ we have:
{{begin-eqn}}
{{eqn	| l = \map f {i a}
		| r = \map {f_0} {\map \Re {i a} } + i \map {f_0} {\map \Im {ia} }
}}
{{eqn	| r = \map {f_0} {-\map \Im a} + i \map {f_0} {\map \Re a}
		| c = Real Part of Imaginary Unit times Element of *-Algebra, Imaginary Part of Imaginary Unit times Element of *-Algebra
}}
{{eqn	| r = i \map {f_0} {\map \Re a} - \map {f_0} {\map \Im a}
		| c = since $f_0$ is linear 
}}
{{eqn	| r = i \paren {\map {f_0} {\map \Re a} + i \map {f_0} {\map \Im a} }
}}
{{eqn	| r = i \map f a
}}
{{end-eqn}}
Now let $a \in A$ and $\lambda \in \R$, we have that:
{{begin-eqn}}
{{eqn	| l = \map f {\lambda a}
		| r = \map {f_0} {\map \Re {\lambda a} } + i \map {f_0} {\map \Im {\lambda a} }
}}
{{eqn	| r = \map {f_0} {\lambda \map \Re a} + i \map {f_0} {\lambda \map \Im a}
		| c = Real Part of Element of *-Algebra is Real Linear and Imaginary Part of Element of *-Algebra is Real Linear
}}
{{eqn	| r = \lambda \paren {\map {f_0} {\map \Re a} + i \map {f_0} {\map \Im a} }
		| c = $f_0$ is linear
}}
{{eqn	| r = \lambda \map f a 
}}
{{end-eqn}}
We also have, for $a, b \in A$:
{{begin-eqn}}
{{eqn	| l = \map f {a + b}
		| r = \map {f_0} {\map \Re {a + b} } + i \map {f_0} {\map \Im {a + b} }
}}
{{eqn	| r = \map {f_0} {\map \Re a + \map \Re b} + i \map {f_0} {\map \Im a + \map \Im b}
		| c = Real Part of Element of *-Algebra is Real Linear and Imaginary Part of Element of *-Algebra is Real Linear
}}
{{eqn	| r = \paren {\map {f_0} {\map \Re a} + i \map {f_0} {\map \Im a} } + \paren {\map {f_0} {\map \Re b} + i \map {f_0} {\map \Im b} }
		| c = $f_0$ is linear
}}
{{eqn	| r = \map f a + \map f b
}}
{{end-eqn}}
Hence for $a, b \in A$ and $\lambda \in \C$ we have:
{{begin-eqn}}
{{eqn	| l = \map f {a + \lambda b}
		| r = \map f a + \map f {\paren {\map \Re \lambda + i \map \Im \lambda} b}
}}
{{eqn	| r = \map f a + \map \Re \lambda \map f b + \map \Im \lambda \map f {i b}
}}
{{eqn	| r = \map f a + \map \Re \lambda \map f b + i \map \Im \lambda \map f b
}}
{{eqn	| r = \map f a + \paren {\map \Re \lambda + i \map \Im \lambda} \map f b
}}
{{eqn	| r = \map f a + \lambda \map f b 
}}
{{end-eqn}}
For $a \in A$ positive, we have:
:$\map f a = \map {f_0} a \ge 0$
Hence $f$ is a positive linear functional.
From Norm of Positive Linear Functional on Unital C*-Algebra, we have:
{{begin-eqn}}
{{eqn	| l = \norm f_{A^\ast} 
		| r = \map f { {\mathbf 1}_A}
}}
{{eqn 	| r = \map {f_1} { {\mathbf 1}_A}
		| c = Identity Element in Unital *-Algebra is Hermitian
}}
{{eqn	| r = \map {f_0} { {\mathbf 1}_B}
		| c = $B$ is unital
}}
{{eqn	| r = \norm {f_0}_{B^\ast}
		| c = Norm of Positive Linear Functional on Unital C*-Algebra
}}
{{eqn	| r = 1
		| c = Norm of Positive Linear Functional on Unital C*-Algebra
}}
{{end-eqn}}
Hence $f$ is a state that extends $f_0$ as required.
{{qed}}