Proofs of some statements from Part 2.

Equivalence of axioms for functions (2.1)

Recalling the axioms:

Fc. ∀t,E, Fnc (E ∋ x ↦ t(x))
1. ∀t,E, ∀Fnc f, f = (E ∋ x ↦ t(x)) ⇔ (Dom f = E ∧ (∀x∈E, f(x) = t(x)))
1'. ∀t,E, ∀f, f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀x∈E, f(x) = t(x))
2. ∀t,E, Dom(E ∋ x ↦ t(x)) = E ∧ ∀y∈E, (E ∋ x ↦ t(x))(y) = t(y)
(=Fnc) ∀Fnc f, ∀Fnc g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g

Splitting the ⇔ in 1. as a conjuction of implications, (1. ⇔ (1a. ∧ 1b.)) where

1a. ∀t,E, ∀Fnc f, f = (E ∋ x ↦ t(x)) ⇒ (Dom f = E ∧ (∀x∈E, f(x) = t(x)))
1b. ∀t,E, ∀Fnc f, (Dom f = E ∧ (∀x∈E, f(x) = t(x))) ⇒ f = (E ∋ x ↦ t(x))

Similarly (1'. ⇔ (1a'. ∧ 1b.)) where
1a'. ∀t,E, ∀ f, f = (E ∋ x ↦ t(x)) ⇒ (Fnc f ∧ Dom f = E ∧ (∀x∈E, f(x) = t(x)))

We can see immediately that 1a'. ⇔ (Fc. ∧ 2.) ⇒ 1a.
(We may write 2. ⇒ 1a. if not careful about definiteness).
Conversely, we can see (1a. ∧ Fc.) ⇒ 2.

Proof of 1b. ⇒ (=Fnc)
∀Fnc f, ∀Fnc g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ ∃SetE, Dom f = E = Dom g ∧ (∀x∈E, f(x) = f(x) = g(x)) ∴ f = (E ∋ x ↦ f(x)) = g.
Proof of (2.∧(=Fnc)) ⇒ 1b. : ∀t,E, ∀Fnc f,
(Dom f = E ∧ (∀x∈E, f(x) = t(x)))
⇒ (Dom f = Dom(E ∋ x ↦ t(x)) ∧ (∀y∈E, f(y) = (E ∋ x ↦ t(x))(y)))
⇒ f = (E ∋ x ↦ t(x))

Equivalence between expressions of the hypothesis of the set generation principle (2.2)

These 3 properties are already known consequences of «Q=∀C ». Conversely,
((2) ∧ (3)) ⇒ ((∀C x, A(x)) ⇒ Qx,A(x))
((1) ∧ ∃C x, A(x)) ⇒ ∃y, (Q*x, x=y) ∧ (∀x, x=y ⇒ A(x)) ∴ ((3) ⇒ Q*x,A(x)) ∎