Line-by-Line First-Order Proof that
g(x) = (3/4)·x² = (3/4)·f(x)

for all x ∈ (0, 3), and hence its graph is a vertical scaling of
f(x) = x² by factor 3/4

---

Proof in First-Order Logic (Field Axioms + Definitions)

We work in a first-order theory of real closed fields with two unary function symbols f, g, a binary multiplication symbol (·), a binary predicate (<), and a division symbol (/). We use inv(a) for the multiplicative inverse of a.

Line	Statement	Justification
1	∀x [0 < x ∧ x < 3 → f(x) = x · x]	Definition of f
2	∀x [0 < x ∧ x < 3 → g(x) = /((3 · f(x)), 4)]	Definition of g
3	∀a,b [/ (a, b) = a · inv(b)]	Axiom: definition of division
4	∀a,b [a · inv(b) = inv(b) · a]	Axiom: commutativity of multiplication
5	∀a,b,c [a · (b · c) = (a · b) · c]	Axiom: associativity of multiplication
6	Let x be arbitrary with 0 < x ∧ x < 3	Universal instantiation (from lines 1, 2)
7	f(x) = x · x	From line 1 and 6
8	g(x) = /((3 · f(x)), 4)	From line 2 and 6
9	g(x) = (3 · f(x)) · inv(4)	From line 3 and 8
10	g(x) = (3 · (x · x)) · inv(4)	From line 7 and 9 (substitute f(x)=x·x)
11	g(x) = (3 · inv(4)) · (x · x)	From line 5 and 10 (re-associate factors)
12	3 · inv(4) = inv(4) · 3	From line 4
13	inv(4) = 1/4	Definition of inv on numeral 4
14	∴ g(x) = (3/4) · (x · x)	From lines 11–13
15	(x · x) = f(x)	From line 7
16	∴ g(x) = (3/4) · f(x)	From lines 14 and 15
17	∴ ∀x [0 < x ∧ x < 3 → g(x) = (3/4) · f(x)]	Universal generalization (from lines 6–16)
18	QED	—

---

Vertical-Scaling Interpretation

The Vertical Scaling Theorem for real functions states:

If h(x) = k·f(x), then the graph of h is obtained by stretching the graph of f by factor k in the y-direction.

Here, k = 3/4. Since we have proved ∀x ∈ (0,3), g(x) = (3/4)·f(x), it follows that the graph of g over (0,3) is exactly the image of the parabola y = x² under a vertical shrink by factor 3/4.