----- Path 1: -----
AXIns   By axiom 'ax1' we know (KN1):
(KN1)   ( x1īreal) ( x2īreal) ( y1īreal) ( y2īreal) ((x1 < y1) & (x2 < y2) => (x1 + x2 < y1 + y2))
AXIns   By axiom 'ax2' we know (KN2):
(KN2)   ( xīreal) ( yīreal) (| x + y | < | x | + | y |)
AXIns   By axiom 'ax3' we know (KN3):
(KN3)   ( xīreal) ( yīreal) ( zīreal) (((x < y) & (y < z)) => (x < z))
        Main goal to prove:
(GOAL)  ( fīnatF) ( gīnatF) (B(f) & B(g) => B(f + g))
I      To show (GOAL) it suffices to show (SG1) for a new constant:
        Let constant 'f' be arbitrary, but fixed.
(SG1)   ( gīnatF) (B(f) & B(g) => B(f + g))
I      To show (SG1) it suffices to show (SG2) for a new constant:
        Let constant 'g' be arbitrary, but fixed.
(SG2)   B(f) & B(g) => B(f + g)
=>I     To show (SG2) it suffices to show (SG3) assuming (ASS1):
(ASS1)  B(f) & B(g)
&E1     By (ASS1) we know (KN4):
(KN4)   B(f)
RDef    By (KN4) and by relation definition 'bDef' we know (KN5):
(KN5)   (EX Sīreal) ( nīnat) (| (f)(n) | < S)
EXE     By (KN5) we may assume (KN6) for a new constant:
        Let constant 'S_f' be such that
(KN6)   ( nīnat) (| (f)(n) | < S_f)
&E2     By (ASS1) we know (KN7):
(KN7)   B(g)
RDef    By (KN7) and by relation definition 'bDef' we know (KN8):
(KN8)   (EX Sīreal) ( nīnat) (| (g)(n) | < S)
EXE     By (KN8) we may assume (KN9) for a new constant:
        Let constant 'S_g' be such that
(KN9)   ( nīnat) (| (g)(n) | < S_g)
(SG3)   B(f + g)
RDef    By (SG3) and by relation definition 'bDef' we have to show (SG4):
(SG4)   (EX Sīreal) ( nīnat) (| (f + g)(n) | < S)
EXI     To show (SG4) it suffices to show (SG5):
        Substitute variable 'S' for term 'S_f+S_g':
(SG5)   ( nīnat) (| (f + g)(n) | < S_f + S_g)
I      To show (SG5) it suffices to show (SG6) for a new constant:
        Let constant 'n' be arbitrary, but fixed.
E      By (KN9) we know (KN10).
        Substitute variable 'n' for term 'n':
(KN10)  | (g)(n) | < S_g
E      By (KN6) we know (KN11).
        Substitute variable 'n' for term 'n':
(KN11)  | (f)(n) | < S_f
&I2     By (KN11) and (KN10) we know (KN12):
(KN12)  (| (f)(n) | < S_f) & (| (g)(n) | < S_g)
E      By (KN1) we know (KN13).
        Substitute variable 'x1' for term '|f(n)|':
(KN13)  ( x2īreal) ( y1īreal) ( y2īreal) ((| f(n) | < y1) & (x2 < y2) => (| f(n) | + x2 < y1 + y2))
E      By (KN13) we know (KN14).
        Substitute variable 'x2' for term '|g(n)|':
(KN14)  ( y1īreal) ( y2īreal) ((| f(n) | < y1) & (| g(n) | < y2) => (| f(n) | + | g(n) | < y1 + y2))
E      By (KN14) we know (KN15).
        Substitute variable 'y1' for term 'S_f':
(KN15)  ( y2īreal) ((| f(n) | < S_f) & (| g(n) | < y2) => (| f(n) | + | g(n) | < S_f + y2))
E      By (KN15) we know (KN16).
        Substitute variable 'y2' for term 'S_g':
(KN16)  (| f(n) | < S_f) & (| g(n) | < S_g) => (| f(n) | + | g(n) | < S_f + S_g)
=>E     By (KN12) and (KN16) we know (KN17):
(KN17)  | f(n) | + | g(n) | < S_f + S_g
E      By (KN2) we know (KN18).
        Substitute variable 'x' for term 'f(n)':
(KN18)  ( yīreal) (| f(n) + y | < | f(n) | + | y |)
E      By (KN18) we know (KN19).
        Substitute variable 'y' for term 'g(n)':
(KN19)  | f(n) + g(n) | < | f(n) | + | g(n) |
&I2     By (KN19) and (KN17) we know (KN20):
(KN20)  (| f(n) + g(n) | < | f(n) | + | g(n) |) & (| f(n) | + | g(n) | < S_f + S_g)
E      By (KN3) we know (KN21).
        Substitute variable 'x' for term '|f(n)+g(n)|':
(KN21)  ( yīreal) ( zīreal) (((| f(n) + g(n) | < y) & (y < z)) => (| f(n) + g(n) | < z))
E      By (KN21) we know (KN22).
        Substitute variable 'y' for term '|f(n)|+|g(n)|':
(KN22)  ( zīreal) (((| f(n) + g(n) | < | f(n) | + | g(n) |) & (| f(n) | + | g(n) | < z)) => (| f(n) + g(n) | < z))
E      By (KN22) we know (KN23).
        Substitute variable 'z' for term 'S_f+S_g':
(KN23)  ((| f(n) + g(n) | < | f(n) | + | g(n) |) & (| f(n) | + | g(n) | < S_f + S_g)) => (| f(n) + g(n) | < S_f + S_g)
=>E     By (KN20) and (KN23) we know (KN24):
(KN24)  | f(n) + g(n) | < S_f + S_g
(SG6)   | (f + g)(n) | < S_f + S_g
RRApp   By (SG6) and by rewrite rule 'rr1' we have to show (SG7):
(SG7)   | f(n) + g(n) | < S_f + S_g
Kn      By (SG7) and (KN24) the path is complete.
(SG8)   <nothing>
----- End of proof-tree -----