Proof of geometric series two-point function

In deriving the expression for the exact propagator

$$G_c^{(2)}(x_1,x_2)=[p^2-m^2+\Pi(p)]^{-1}$$

for $$\phi^4$$ theory all books that i know use the following argument:

$$G_c^{(2)}(x_1,x_2)=G_0^{(2)}+G_0^{(2)}\Pi G_0^{(2)}+G_0^{(2)}\Pi G_0^{(2)}\Pi G_0^{(2)}+\ldots .$$

Here $$\Pi$$ is the sum of all irreducible diagrams.

Using Feynman diagrams to the lower order we can see that this is true, but what about the higher orders? Is there any formal proof (by induction or something else) that this true?

Sketched proof:

1. In general we know that a connected diagram is a tree of bare propagators $$G_0$$ and (amputated) 1PI vertices, cf. Lemma 3.11 in Ref. 1.

2. In particular, the full propagator/connected 2-pt function $$G_c$$ must be strings of bare propagators $$G_0$$ and (amputated) 2-pt vertex $$\Sigma\equiv \Pi$$, which we call self-energy.

3. Now what about the coefficients in front of each Feynman diagram? Due to the combinatorics/factorization involved it becomes a geometric series $$G_c~=~G_0\sum_{n=0}^{\infty}(\Sigma G_0)^n.\tag{A}$$

4. We can isolate the (amputated) 2-pt 1PI vertices in eq. (A) $$\Sigma~=~G_0^{-1}-G_c^{-1}.\tag{B}$$

5. In general the self-energy $$\Sigma$$ consists of connected diagrams with 2 amputated legs such that the 2 legs cannot be disconnected by cutting a single internal line.

6. If there are no tadpoles, the self-energy $$\Sigma$$ is 1PI, cf. my Phys.SE answer here.

References:

1. P. Etingof, Geometry & QFT, MIT 2002 online lecture notes; Sections 3.11 & 3.12.