Let (v,z_n, ..., z₀) e EFPN. We want to prove that f(g(v,z_n, ..., z_0))=:(v',z_n', ..., z_0')=(v,z_n, ..., z_0).

We have SUM_i=0ⁿ (z_i ·PROD_j=0^i-1 M_j) > 0, as all z_i > 0 and all M_j > 2.

Thus

v=1

implies g(v,z_n, ..., z₀) > 0 and therefore v'=1, and

v=-1

implies g(v,z_n, ..., z₀) < 0 (here we need that the zero in EFPN is unique, i.e. can only have the sign "1") and therefore v'=-1.

For the rest of this subsection we assume v=1. Under this assumption is remains to show that

1. (SUM_i=0ⁿ (z_i ·PROD_j=0^i-1 M_j)) div PROD_j=0^n-1 M_j = z_n and
2. ((SUM_i=0ⁿ (z_i ·PROD_j=0^i-1 M_j)) div PROD_j=0^x-1 M_j ) mod M_x = z_x, 0 < x < n.

ad 1.

As z_i < M_i for 0 < i < n we can size up z_i ·PROD_j=0^i-1 M_j < PROD_j=0ⁱ M_j. Thus under the div-operator for i=0 to n-1 all terms of the sum lead to zero - only the last one remains and results in (z_n ·PROD_j=0^n-1 M_j) div PROD_j=0^n-1 M_j = z_n.

ad 2.

We consider the terms of three distinct parts of the sum depending on the actual index y of a term:

x < y < n:

	( (zy ·PRODj=0y-1 Mj) div PRODj=0x-1 Mj ) mod Mx
=	( zy ·Mx ·PRODj=x+1y-1 Mj ) mod Mx
=	0.

x=y:

	( (zx ·PRODj=0x-1 Mj) div PRODj=0x-1 Mj ) mod Mx
=	zx mod Mx
=	zx.

The last step is valid as z_x e {0,1,..., M_x -1}.

0 < y <x:

We size up as follows: z_y ·PROD_j=0^y-1 M_j < PROD_j=0^y M_j < PROD_j=0^x-1 M_j. Therefore

	( (zy ·PRODj=0y-1 Mj) div PRODj=0x-1 Mj ) mod Mx
=	0 mod Mx
=	0.