For proving [Graphics:submitted.nbgr138.gif] we prove, for arbitrary but fixed values,

[Graphics:submitted.nbgr139.gif] [Graphics:submitted.nbgr140.gif].

We prove [Graphics:submitted.nbgr141.gif] by the deduction rule.

We assume

[Graphics:submitted.nbgr142.gif] [Graphics:submitted.nbgr143.gif]

and show

[Graphics:submitted.nbgr144.gif] [Graphics:submitted.nbgr145.gif].

From [Graphics:submitted.nbgr146.gif] and [Graphics:submitted.nbgr147.gif] we obtain by modus ponens

[Graphics:submitted.nbgr148.gif] [Graphics:submitted.nbgr149.gif].

By [Graphics:submitted.nbgr150.gif] we can take appropriate values such that

[Graphics:submitted.nbgr151.gif] [Graphics:submitted.nbgr152.gif].

From [Graphics:submitted.nbgr153.gif] and [Graphics:submitted.nbgr154.gif] we obtain by modus ponens

[Graphics:submitted.nbgr155.gif] [Graphics:submitted.nbgr156.gif].

From [Graphics:submitted.nbgr157.gif] and [Graphics:submitted.nbgr158.gif] we obtain by modus ponens

[Graphics:submitted.nbgr159.gif] [Graphics:submitted.nbgr160.gif].

By [Graphics:submitted.nbgr161.gif] we can take appropriate values such that

[Graphics:submitted.nbgr162.gif] [Graphics:submitted.nbgr163.gif].

By [Graphics:submitted.nbgr164.gif] we can take appropriate values such that

[Graphics:submitted.nbgr165.gif] [Graphics:submitted.nbgr166.gif].

We prove first

[Graphics:submitted.nbgr167.gif] [Graphics:submitted.nbgr168.gif].

For proving [Graphics:submitted.nbgr256.gif] we prove, for arbitrary but fixed values,

Formula [Graphics:submitted.nbgr257.gif] is proved because [Graphics:submitted.nbgr258.gif]is an instance of it.