\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{HAL006+1.p} Lemma for the short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists r,b_1{:}\;( \mbox{element}(r,r)\mbox{ and }\mbox{apply}(\mbox{delta},e) = r\mbox{ and }\mbox{element}(b_1,b)\mbox{ and }\mbox{apply}(h,\mbox{apply}(\mbox{beta},b_1)) = r\mbox{ and }\mbox{apply}(\mbox{delta},\mbox{apply}(g,b_1)) = r ) )\qquad\mbox{fof}(\mbox{lemma}_3,\mbox{axiom})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists b_1,e_1,a{:}\;( \mbox{element}(b_1,b)\mbox{ and }\mbox{element}(e_1,e)\mbox{ and }\mbox{subtract}(e,\mbox{apply}(g,b_1),e) = e_1\mbox{ and }\mbox{element}(a,a)\mbox{ and }\mbox{apply}(\mbox{gamma},\mbox{apply}(f,a)) = e_1\mbox{ and }\mbox{apply}(g,\mbox{apply}(\mbox{alpha},a)) = e_1 ) )\qquad\mbox{fof}(\mbox{lemma}_8,\mbox{axiom})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists b_1,b_2{:}\;( \mbox{element}(b_1,b)\mbox{ and }\mbox{element}(b_2,b)\mbox{ and }\mbox{apply}(g,\mbox{subtract}(b,b_1,b_2)) = e ) )\qquad\mbox{fof}(\mbox{lemma}_{12},\mbox{conjecture})$

\medskip\textbf{HAL007+1.p} Standard homological algebra axioms






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

\medskip\textbf{HAL004+1.p} Lemma for the short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists r,b_1{:}\;( \mbox{element}(r,r)\mbox{ and }\mbox{apply}(\mbox{delta},e) = r\mbox{ and }\mbox{element}(b_1,b)\mbox{ and }\mbox{apply}(h,\mbox{apply}(\mbox{beta},b_1)) = r\mbox{ and }\mbox{apply}(\mbox{delta},\mbox{apply}(g,b_1)) = r ) )\qquad\mbox{fof}(\mbox{lemma}_3,\mbox{conjecture})$

\medskip\textbf{HAL005+1.p} Lemma for the short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists r,b_1{:}\;( \mbox{element}(r,r)\mbox{ and }\mbox{apply}(\mbox{delta},e) = r\mbox{ and }\mbox{element}(b_1,b)\mbox{ and }\mbox{apply}(h,\mbox{apply}(\mbox{beta},b_1)) = r\mbox{ and }\mbox{apply}(\mbox{delta},\mbox{apply}(g,b_1)) = r ) )\qquad\mbox{fof}(\mbox{lemma}_3,\mbox{axiom})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists b_1,e_1,a{:}\;( \mbox{element}(b_1,b)\mbox{ and }\mbox{element}(e_1,e)\mbox{ and }\mbox{subtract}(e,\mbox{apply}(g,b_1),e) = e_1\mbox{ and }\mbox{element}(a,a)\mbox{ and }\mbox{apply}(\mbox{gamma},\mbox{apply}(f,a)) = e_1\mbox{ and }\mbox{apply}(g,\mbox{apply}(\mbox{alpha},a)) = e_1 ) )\qquad\mbox{fof}(\mbox{lemma}_8,\mbox{conjecture})$

\medskip\textbf{HAL003+3.p} Short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists r,b_1{:}\;( \mbox{element}(r,r)\mbox{ and }\mbox{apply}(\mbox{delta},e) = r\mbox{ and }\mbox{element}(b_1,b)\mbox{ and }\mbox{apply}(h,\mbox{apply}(\mbox{beta},b_1)) = r\mbox{ and }\mbox{apply}(\mbox{delta},\mbox{apply}(g,b_1)) = r ) )\qquad\mbox{fof}(\mbox{lemma}_3,\mbox{axiom})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists b_1,e_1,a{:}\;( \mbox{element}(b_1,b)\mbox{ and }\mbox{element}(e_1,e)\mbox{ and }\mbox{subtract}(e,\mbox{apply}(g,b_1),e) = e_1\mbox{ and }\mbox{element}(a,a)\mbox{ and }\mbox{apply}(\mbox{gamma},\mbox{apply}(f,a)) = e_1\mbox{ and }\mbox{apply}(g,\mbox{apply}(\mbox{alpha},a)) = e_1 ) )\qquad\mbox{fof}(\mbox{lemma}_8,\mbox{axiom})$

$\forall e{:}\;( \mbox{element}(e,e) \ \Rightarrow \ \exists b_1,b_2{:}\;( \mbox{element}(b_1,b)\mbox{ and }\mbox{element}(b_2,b)\mbox{ and }\mbox{apply}(g,\mbox{subtract}(b,b_1,b_2)) = e ) )\qquad\mbox{fof}(\mbox{lemma}_{12},\mbox{axiom})$

$\mbox{surjection}(g)\qquad\mbox{fof}(\mbox{g\_surjection},\mbox{conjecture})$

\medskip\textbf{HAL003+1.p} Short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(g)\qquad\mbox{fof}(\mbox{g\_surjection},\mbox{conjecture})$

\medskip\textbf{HAL001+1.p} Short Five Lemma, Part 1






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{injection}(f)\qquad\mbox{fof}(\mbox{f\_injection},\mbox{hypothesis})$

$\mbox{injection}(h)\qquad\mbox{fof}(\mbox{h\_injection},\mbox{hypothesis})$

$\mbox{injection}(g)\qquad\mbox{fof}(\mbox{g\_injection},\mbox{conjecture})$

\medskip\textbf{HAL002+1.p} Equivalence of injection axioms






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\forall \mbox{morphism},\mbox{dom},\mbox{cod}{:}\;( ( \mbox{injection}_2(\mbox{morphism})\mbox{ and }\mbox{morphism}(\mbox{morphism},\mbox{dom},\mbox{cod}) ) \ \Rightarrow \ \forall \mbox{el}{:}\;( ( \mbox{element}(\mbox{el},\mbox{dom})\mbox{ and }\mbox{apply}(\mbox{morphism},\mbox{el}) = 0 ) \ \Rightarrow \ \mbox{el} = 0 ) )\qquad\mbox{fof}(\mbox{injection\_properties}_2,\mbox{axiom})$

$\forall \mbox{morphism},\mbox{dom},\mbox{cod}{:}\;( ( \mbox{morphism}(\mbox{morphism},\mbox{dom},\mbox{cod})\mbox{ and }\forall \mbox{el}{:}\;( ( \mbox{element}(\mbox{el},\mbox{dom})\mbox{ and }\mbox{apply}(\mbox{morphism},\mbox{el}) = 0 ) \ \Rightarrow \ \mbox{el} = 0 ) ) \ \Rightarrow \ \mbox{injection}_2(\mbox{morphism}) )\qquad\mbox{fof}(\mbox{properties\_for\_injection}_2,\mbox{axiom})$

$\mbox{morphism}(x,\mbox{any}_1,\mbox{any}_2)\qquad\mbox{fof}(\mbox{x\_morphism},\mbox{hypothesis})$

$\mbox{injection}(x)\iff \mbox{injection}_2(x)\qquad\mbox{fof}(\mbox{my},\mbox{conjecture})$

\medskip\textbf{HAL003+2.p} Short Five Lemma, Part 2






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{surjection}(f)\qquad\mbox{fof}(\mbox{f\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(h)\qquad\mbox{fof}(\mbox{h\_surjection},\mbox{hypothesis})$

$\mbox{surjection}(g)\qquad\mbox{fof}(\mbox{g\_surjection},\mbox{conjecture})$

\medskip\textbf{HAL001+2.p} Short Five Lemma, Part 1






$\mbox{include}(\mbox{'Axioms/HAL001+0.ax'})$

$\forall \mbox{morphism},\mbox{dom},\mbox{cod}{:}\;( ( \mbox{injection}(\mbox{morphism})\mbox{ and }\mbox{morphism}(\mbox{morphism},\mbox{dom},\mbox{cod}) ) \ \Rightarrow \ \forall \mbox{el}{:}\;( ( \mbox{element}(\mbox{el},\mbox{dom})\mbox{ and }\mbox{apply}(\mbox{morphism},\mbox{el}) = 0 ) \ \Rightarrow \ \mbox{el} = 0 ) )\qquad\mbox{fof}(\mbox{injection\_properties}_2,\mbox{axiom})$

$\forall \mbox{morphism},\mbox{dom},\mbox{cod}{:}\;( ( \mbox{morphism}(\mbox{morphism},\mbox{dom},\mbox{cod})\mbox{ and }\forall \mbox{el}{:}\;( ( \mbox{element}(\mbox{el},\mbox{dom})\mbox{ and }\mbox{apply}(\mbox{morphism},\mbox{el}) = 0 ) \ \Rightarrow \ \mbox{el} = 0 ) ) \ \Rightarrow \ \mbox{injection}(\mbox{morphism}) )\qquad\mbox{fof}(\mbox{properties\_for\_injection}_2,\mbox{axiom})$

$\mbox{morphism}(\mbox{alpha},a,b)\qquad\mbox{fof}(\mbox{alpha\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{beta},b,c)\qquad\mbox{fof}(\mbox{beta\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{gamma},d,e)\qquad\mbox{fof}(\mbox{gamma\_morphism},\mbox{axiom})$

$\mbox{morphism}(\mbox{delta},e,r)\qquad\mbox{fof}(\mbox{delta\_morphism},\mbox{axiom})$

$\mbox{morphism}(f,a,d)\qquad\mbox{fof}(\mbox{f\_morphism},\mbox{axiom})$

$\mbox{morphism}(g,b,e)\qquad\mbox{fof}(\mbox{g\_morphism},\mbox{axiom})$

$\mbox{morphism}(h,c,r)\qquad\mbox{fof}(\mbox{h\_morphism},\mbox{axiom})$

$\mbox{injection}(\mbox{alpha})\qquad\mbox{fof}(\mbox{alpha\_injection},\mbox{axiom})$

$\mbox{injection}(\mbox{gamma})\qquad\mbox{fof}(\mbox{gamma\_injection},\mbox{axiom})$

$\mbox{surjection}(\mbox{beta})\qquad\mbox{fof}(\mbox{beta\_surjection},\mbox{axiom})$

$\mbox{surjection}(\mbox{delta})\qquad\mbox{fof}(\mbox{delta\_surjection},\mbox{axiom})$

$\mbox{exact}(\mbox{alpha},\mbox{beta})\qquad\mbox{fof}(\mbox{alpha\_beta\_exact},\mbox{axiom})$

$\mbox{exact}(\mbox{gammma},\mbox{delta})\qquad\mbox{fof}(\mbox{gamma\_delta\_exact},\mbox{axiom})$

$\mbox{commute}(\mbox{alpha},g,f,\mbox{gamma})\qquad\mbox{fof}(\mbox{alpha\_g\_f\_gamma\_commute},\mbox{axiom})$

$\mbox{commute}(\mbox{beta},h,g,\mbox{delta})\qquad\mbox{fof}(\mbox{beta\_h\_g\_delta\_commute},\mbox{axiom})$

$\mbox{injection}(f)\qquad\mbox{fof}(\mbox{f\_injection},\mbox{hypothesis})$

$\mbox{injection}(h)\qquad\mbox{fof}(\mbox{h\_injection},\mbox{hypothesis})$

$\mbox{injection}(g)\qquad\mbox{fof}(\mbox{g\_injection},\mbox{conjecture})$

\medskip
\end{document}