LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If $f$ and $g$ are functions then $g \circ f$ is a function with domain $f^{-1}[\operatorname{dom} g]$ and $(g \circ f)(x) = g(f(x))$ there; $\Delta_A$ is a function with $\Delta_A(a) = a$ ; and $f \circ \Delta_A = f = \Delta_B \circ f$ for $f : A \to B$

Statement

Let $f$ and $g$ be functions and let $A$ , $B$ be sets. Then

(i) $g \circ f$ is a function, $\operatorname{dom}(g \circ f) = f^{-1}[\operatorname{dom} g]$ , and $(g \circ f)(x) = g(f(x))$ for every $x$ in that domain;
(ii) $\Delta_A$ is a function with $\operatorname{dom} \Delta_A = A$ and $\Delta_A(a) = a$ for every $a \in A$ ;
(iii) if $f : A \to B$ then $f \circ \Delta_A = f$ and $\Delta_B \circ f = f$ .

Facts & Assumptions

Given: functions $f$ and $g$ , and sets $A$ , $B$ .

[L1]

A function is a relation $f$ such that $(a,b) \in f$ and $(a,c) \in f$ imply $b = c$ (A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f(a)$ , domain and codomain).

[L2]

$(a,c) \in S \circ R$ holds if and only if $(a,b) \in R$ and $(b,c) \in S$ for some $b$ (The inverse relation $R^{-1}$ , the composite $S \circ R$ , and the restriction $R \restriction A$ ).

[L3]

$\operatorname{dom} R := \{\, a : \exists b\ (a,b) \in R \,\}$ (Relation, $\operatorname{dom} R$ , $\operatorname{ran} R$ , $\operatorname{fld} R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L4]

$a \in R^{-1}[B]$ holds if and only if $(a,b) \in R$ for some $b \in B$ (The image $R[A]$ and the preimage $R^{-1}[B]$ of a set under a relation).

[L5]

$(a,b) \in \Delta_A$ holds if and only if $a = b$ and $a \in A$ (The identity relation $\Delta_A = \{\,(a,b) \in A \times A : a = b\,\}$ and the membership relation $\in_A\, = \{\,(a,b) \in A \times A : a \in b\,\}$ ).

[L6]

if $R$ is a relation from $A$ to $B$ , then $\Delta_B \circ R = R$ and $R \circ \Delta_A = R$ ( $T \circ (S \circ R) = (T \circ S) \circ R$ , $(S \circ R)^{-1} = R^{-1} \circ S^{-1}$ , $(R^{-1})^{-1} = R$ , $\operatorname{dom}(R^{-1}) = \operatorname{ran} R$ , and $\Delta_B \circ R = R = R \circ \Delta_A$ for a relation $R$ from $A$ to $B$ ).

Proof

technique · direct

1.1

Claim (i), single-valuedness: $g \circ f$ is a relation, and if $(a,c)$ and $(a,c')$ both lie in it, there are $b$ and $b'$ with $(a,b),(a,b') \in f$ and $(b,c),(b',c') \in g$ ; single-valuedness of $f$ gives $b = b'$ , and then single-valuedness of $g$ gives $c = c'$ .

L1L2

1.2

Claim (ii): if $(a,b)$ and $(a,c)$ lie in $\Delta_A$ then $b = a = c$ , so $\Delta_A$ is a function; its domain is $A$ , because $(a,a) \in \Delta_A$ exactly for $a \in A$ , and its value at $a$ is $a$ .

L1L3L5

1.3

Claim (iii): a function $f : A \to B$ has $\operatorname{dom} f = A$ and $\operatorname{ran} f \subseteq B$ , so it is a relation from $A$ to $B$ , and the identity laws for relations apply verbatim.

2.1

Claim (i), domain and values: $a \in \operatorname{dom}(g \circ f)$ holds exactly when there are $b$ and $c$ with $(a,b) \in f$ and $(b,c) \in g$ , that is, exactly when $a \in \operatorname{dom} f$ and $f(a) \in \operatorname{dom} g$ ; and that is exactly the condition $a \in f^{-1}[\operatorname{dom} g]$ . For such an $a$ the pair $(a, g(f(a)))$ lies in $g \circ f$ , so $(g \circ f)(a) = g(f(a))$ by step 1.1.

L1L2L3L4step 1.1

3.1

Claims (i), (ii) and (iii) are established, which is the statement.

step 1.1step 1.2step 1.3step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

B. Kaya, MATH 320 Set Theory (METU), Lemma 5 and Exercise 11 (standard reference, not scraped)
Function composition (Wikipedia) (standard reference, not scraped)
Function (mathematics) (Wikipedia) (standard reference, not scraped)