:: Arithmetic Operations on Functions from Sets into Functional Sets :: by Artur Korni{\l}owicz :: :: Received October 15, 2008 :: Copyright (c) 2008-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, FUNCT_1, TARSKI, RELAT_1, SUBSET_1, VALUED_0, PARTFUN1, FUNCT_2, MEMBERED, XCMPLX_0, ARYTM_3, ARYTM_1, VALUED_1, RAT_1, FINSEQ_1, NAT_1, COMPLEX1, INT_1, VALUED_2, FUNCOP_1, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, BINOP_1, VALUED_0, VALUED_1, INT_1, NAT_1, XCMPLX_0, XREAL_0, RAT_1, MEMBERED, FINSEQ_1; constructors RELAT_2, PARTFUN1, MCART_1, FUNCT_2, VALUED_0, VALUED_1, NAT_1, ARYTM_0, XCMPLX_0, FINSEQ_1, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0, COMPLEX1, RELSET_1, FUNCOP_1, BINOP_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, RELSET_1, MEMBERED, ORDINAL1, XCMPLX_0, NUMBERS, RAT_1, XREAL_0, INT_1; requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL; definitions TARSKI, FUNCT_1, FUNCOP_1; equalities XCMPLX_0, VALUED_1, BINOP_1, ORDINAL1; expansions TARSKI; theorems TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, XCMPLX_1, XBOOLE_0, XBOOLE_1, RFUNCT_1, FINSEQ_1, RELAT_1, ZFMISC_1, XCMPLX_0, XREAL_0, RAT_1, INT_1, ORDINAL1; schemes XBOOLE_0, FUNCT_1, CLASSES1; begin :: Functional sets reserve x, y for object, X, X1, X2 for set; Lm1: now let X1,X2,X3 be set; thus X1 /\ (X2 /\ X3) = X1 /\ X1 /\ X2 /\ X3 by XBOOLE_1:16 .= X1 /\ (X1 /\ X2) /\ X3 by XBOOLE_1:16 .= (X1 /\ X2) /\ (X1 /\ X3) by XBOOLE_1:16; end; definition let Y be functional set; func DOMS(Y) -> set equals union the set of all dom f where f is Element of Y; coherence; end; definition let X; attr X is complex-functions-membered means :Def2: x in X implies x is complex-valued Function; end; definition let X; attr X is ext-real-functions-membered means :Def3: x in X implies x is ext-real-valued Function; end; definition let X; attr X is real-functions-membered means :Def4: x in X implies x is real-valued Function; end; definition let X; attr X is rational-functions-membered means :Def5: x in X implies x is RAT-valued Function; end; definition let X; attr X is integer-functions-membered means :Def6: x in X implies x is INT-valued Function; end; definition let X; attr X is natural-functions-membered means :Def7: x in X implies x is natural-valued Function; end; registration cluster natural-functions-membered -> integer-functions-membered for set; coherence proof let X; assume A1: for x being object st x in X holds x is natural-valued Function; let x; assume x in X; then x is natural-valued Function by A1; hence thesis; end; cluster integer-functions-membered -> rational-functions-membered for set; coherence proof let X; assume A2: for x being object st x in X holds x is INT-valued Function; let x; assume x in X; then x is INT-valued Function by A2; hence thesis; end; cluster rational-functions-membered -> real-functions-membered for set; coherence; cluster real-functions-membered -> complex-functions-membered for set; coherence; cluster real-functions-membered -> ext-real-functions-membered for set; coherence; end; registration cluster empty -> natural-functions-membered for set; coherence; end; registration let f be complex-valued Function; cluster {f} -> complex-functions-membered; coherence by TARSKI:def 1; end; registration cluster complex-functions-membered -> functional for set; coherence proof let X; assume A1: X is complex-functions-membered; let x; thus thesis by A1; end; cluster ext-real-functions-membered -> functional for set; coherence proof let X; assume A2: X is ext-real-functions-membered; let x; thus thesis by A2; end; end; set ff = the natural-valued Function; registration cluster natural-functions-membered non empty for set; existence proof take {ff}; thus for x being object st x in {ff} holds x is natural-valued Function by TARSKI:def 1; thus thesis; end; end; registration let X be complex-functions-membered set; cluster -> complex-functions-membered for Subset of X; coherence by Def2; end; registration let X be ext-real-functions-membered set; cluster -> ext-real-functions-membered for Subset of X; coherence by Def3; end; registration let X be real-functions-membered set; cluster -> real-functions-membered for Subset of X; coherence by Def4; end; registration let X be rational-functions-membered set; cluster -> rational-functions-membered for Subset of X; coherence by Def5; end; registration let X be integer-functions-membered set; cluster -> integer-functions-membered for Subset of X; coherence by Def6; end; registration let X be natural-functions-membered set; cluster -> natural-functions-membered for Subset of X; coherence by Def7; end; definition set A = COMPLEX; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func C_PFuncs(D) -> set means :Def8: for f being object holds f in it iff f is PartFunc of D,COMPLEX; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = COMPLEX; let D be set; defpred P[object] means \$1 is Function of D,A; func C_Funcs(D) -> set means :Def9: for f being object holds f in it iff f is Function of D,COMPLEX; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = ExtREAL; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func E_PFuncs(D) -> set means :Def10: for f being object holds f in it iff f is PartFunc of D,ExtREAL; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = ExtREAL; let D be set; defpred P[object] means \$1 is Function of D,A; func E_Funcs(D) -> set means :Def11: for f being object holds f in it iff f is Function of D,ExtREAL; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = REAL; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func R_PFuncs(D) -> set means :Def12: for f being object holds f in it iff f is PartFunc of D,REAL; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = REAL; let D be set; defpred P[object] means \$1 is Function of D,A; func R_Funcs(D) -> set means :Def13: for f being object holds f in it iff f is Function of D,REAL; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = RAT; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func Q_PFuncs(D) -> set means :Def14: for f being object holds f in it iff f is PartFunc of D,RAT; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = RAT; let D be set; defpred P[object] means \$1 is Function of D,A; func Q_Funcs(D) -> set means :Def15: for f being object holds f in it iff f is Function of D,RAT; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = INT; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func I_PFuncs(D) -> set means :Def16: for f being object holds f in it iff f is PartFunc of D,INT; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = INT; let D be set; defpred P[object] means \$1 is Function of D,A; func I_Funcs(D) -> set means :Def17: for f being object holds f in it iff f is Function of D,INT; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = NAT; let D be set; defpred P[object] means \$1 is PartFunc of D,A; func N_PFuncs(D) -> set means :Def18: for f being object holds f in it iff f is PartFunc of D,NAT; existence proof consider X being set such that A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is PartFunc of D,A by A1; assume A2: f is PartFunc of D,A; then f in PFuncs(D,A) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is PartFunc of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is PartFunc of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; definition set A = NAT; let D be set; defpred P[object] means \$1 is Function of D,A; func N_Funcs(D) -> set means :Def19: for f being object holds f in it iff f is Function of D,NAT; existence proof consider X being set such that A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from XBOOLE_0:sch 1; take X; let f be object; thus f in X implies f is Function of D,A by A1; assume A2: f is Function of D,A; then f in Funcs(D,A) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let P, Q be set; assume for f being object holds f in P iff f is Function of D,A; then A3: for f being object holds f in P iff P[f]; assume for f being object holds f in Q iff f is Function of D,A; then A4: for f being object holds f in Q iff P[f]; thus P = Q from XBOOLE_0:sch 2(A3,A4); end; end; theorem Th1: C_Funcs(X) is Subset of C_PFuncs(X) proof C_Funcs(X) c= C_PFuncs(X) proof let x be object; assume x in C_Funcs(X); then x is Function of X,COMPLEX by Def9; hence thesis by Def8; end; hence thesis; end; theorem Th2: E_Funcs(X) is Subset of E_PFuncs(X) proof E_Funcs(X) c= E_PFuncs(X) proof let x be object; assume x in E_Funcs(X); then x is Function of X,ExtREAL by Def11; hence thesis by Def10; end; hence thesis; end; theorem Th3: R_Funcs(X) is Subset of R_PFuncs(X) proof R_Funcs(X) c= R_PFuncs(X) proof let x be object; assume x in R_Funcs(X); then x is Function of X,REAL by Def13; hence thesis by Def12; end; hence thesis; end; theorem Th4: Q_Funcs(X) is Subset of Q_PFuncs(X) proof Q_Funcs(X) c= Q_PFuncs(X) proof let x be object; assume x in Q_Funcs(X); then x is Function of X,RAT by Def15; hence thesis by Def14; end; hence thesis; end; theorem Th5: I_Funcs(X) is Subset of I_PFuncs(X) proof I_Funcs(X) c= I_PFuncs(X) proof let x be object; assume x in I_Funcs(X); then x is Function of X,INT by Def17; hence thesis by Def16; end; hence thesis; end; theorem Th6: N_Funcs(X) is Subset of N_PFuncs(X) proof N_Funcs(X) c= N_PFuncs(X) proof let x be object; assume x in N_Funcs(X); then x is Function of X,NAT by Def19; hence thesis by Def18; end; hence thesis; end; registration let X; cluster C_PFuncs(X) -> complex-functions-membered; coherence by Def8; cluster C_Funcs(X) -> complex-functions-membered; coherence proof reconsider C = C_Funcs(X) as Subset of C_PFuncs(X) by Th1; C is complex-functions-membered; hence thesis; end; cluster E_PFuncs(X) -> ext-real-functions-membered; coherence by Def10; cluster E_Funcs(X) -> ext-real-functions-membered; coherence proof reconsider C = E_Funcs(X) as Subset of E_PFuncs(X) by Th2; C is ext-real-functions-membered; hence thesis; end; cluster R_PFuncs(X) -> real-functions-membered; coherence by Def12; cluster R_Funcs(X) -> real-functions-membered; coherence proof reconsider C = R_Funcs(X) as Subset of R_PFuncs(X) by Th3; C is real-functions-membered; hence thesis; end; cluster Q_PFuncs(X) -> rational-functions-membered; coherence by Def14; cluster Q_Funcs(X) -> rational-functions-membered; coherence proof reconsider C = Q_Funcs(X) as Subset of Q_PFuncs(X) by Th4; C is rational-functions-membered; hence thesis; end; cluster I_PFuncs(X) -> integer-functions-membered; coherence by Def16; cluster I_Funcs(X) -> integer-functions-membered; coherence proof reconsider C = I_Funcs(X) as Subset of I_PFuncs(X) by Th5; C is integer-functions-membered; hence thesis; end; cluster N_PFuncs(X) -> natural-functions-membered; coherence by Def18; cluster N_Funcs(X) -> natural-functions-membered; coherence proof reconsider C = N_Funcs(X) as Subset of N_PFuncs(X) by Th6; C is natural-functions-membered; hence thesis; end; end; registration let X be complex-functions-membered set; cluster -> complex-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def2,SUBSET_1:def 1; end; end; registration let X be ext-real-functions-membered set; cluster -> ext-real-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def3,SUBSET_1:def 1; end; end; registration let X be real-functions-membered set; cluster -> real-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def4,SUBSET_1:def 1; end; end; registration let X be rational-functions-membered set; cluster -> RAT-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def5,SUBSET_1:def 1; end; end; registration let X be integer-functions-membered set; cluster -> INT-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def6,SUBSET_1:def 1; end; end; registration let X be natural-functions-membered set; cluster -> natural-valued for Element of X; coherence proof X is empty or X is non empty; hence thesis by Def7,SUBSET_1:def 1; end; end; registration let X be set, x be object; let Y be complex-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> Function-like Relation-like; coherence; end; registration let X be set, x be object; let Y be ext-real-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> Function-like Relation-like; coherence; end; registration let X be set, x be object; let Y be complex-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> complex-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X be set, x be object; let Y be ext-real-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> ext-real-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X be set, x be object; let Y be real-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> real-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X be set, x be object; let Y be rational-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> RAT-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X be set, x be object; let Y be integer-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> INT-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X be set, x be object; let Y be natural-functions-membered set; let f be PartFunc of X,Y; cluster f.x -> natural-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let X; let Y be complex-membered set; cluster PFuncs(X,Y) -> complex-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be ext-real-membered set; cluster PFuncs(X,Y) -> ext-real-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be real-membered set; cluster PFuncs(X,Y) -> real-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be rational-membered set; cluster PFuncs(X,Y) -> rational-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be integer-membered set; cluster PFuncs(X,Y) -> integer-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be natural-membered set; cluster PFuncs(X,Y) -> natural-functions-membered; coherence proof let x; assume x in PFuncs(X,Y); then consider f being Function such that A1: x = f and A2: dom f c= X & rng f c= Y by PARTFUN1:def 3; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be complex-membered set; cluster Funcs(X,Y) -> complex-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be ext-real-membered set; cluster Funcs(X,Y) -> ext-real-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be real-membered set; cluster Funcs(X,Y) -> real-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be rational-membered set; cluster Funcs(X,Y) -> rational-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be integer-membered set; cluster Funcs(X,Y) -> integer-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; registration let X; let Y be natural-membered set; cluster Funcs(X,Y) -> natural-functions-membered; coherence proof let x; assume x in Funcs(X,Y); then consider f being Function such that A1: x = f and A2: dom f = X & rng f c= Y by FUNCT_2:def 2; reconsider f as PartFunc of X,Y by A2,RELSET_1:4; f is set; hence thesis by A1; end; end; definition let R be Relation; attr R is complex-functions-valued means :Def20: rng R is complex-functions-membered; attr R is ext-real-functions-valued means :Def21: rng R is ext-real-functions-membered; attr R is real-functions-valued means :Def22: rng R is real-functions-membered; attr R is rational-functions-valued means :Def23: rng R is rational-functions-membered; attr R is integer-functions-valued means :Def24: rng R is integer-functions-membered; attr R is natural-functions-valued means :Def25: rng R is natural-functions-membered; end; registration let Y be complex-functions-membered set; cluster -> complex-functions-valued for Y-valued Function; coherence proof let f be Y-valued Function; thus rng f is complex-functions-membered; end; end; definition let f be Function; redefine attr f is complex-functions-valued means for x being object st x in dom f holds f.x is complex-valued Function; compatibility proof thus f is complex-functions-valued implies for x being object st x in dom f holds f.x is complex-valued Function proof assume A1: rng f is complex-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A1; end; assume A2: for x being object st x in dom f holds f.x is complex-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A2; end; redefine attr f is ext-real-functions-valued means for x being object st x in dom f holds f.x is ext-real-valued Function; compatibility proof thus f is ext-real-functions-valued implies for x being object st x in dom f holds f.x is ext-real-valued Function proof assume A3: rng f is ext-real-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A3; end; assume A4: for x being object st x in dom f holds f.x is ext-real-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A4; end; redefine attr f is real-functions-valued means for x being object st x in dom f holds f.x is real-valued Function; compatibility proof thus f is real-functions-valued implies for x being object st x in dom f holds f.x is real-valued Function proof assume A5: rng f is real-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A5; end; assume A6: for x being object st x in dom f holds f.x is real-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A6; end; redefine attr f is rational-functions-valued means for x being object st x in dom f holds f.x is RAT-valued Function; compatibility proof thus f is rational-functions-valued implies for x being object st x in dom f holds f.x is RAT-valued Function proof assume A7: rng f is rational-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A7; end; assume A8: for x being object st x in dom f holds f.x is RAT-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A8; end; redefine attr f is integer-functions-valued means for x being object st x in dom f holds f.x is INT-valued Function; compatibility proof thus f is integer-functions-valued implies for x being object st x in dom f holds f.x is INT-valued Function proof assume A9: rng f is integer-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A9; end; assume A10: for x being object st x in dom f holds f.x is INT-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A10; end; redefine attr f is natural-functions-valued means for x being object st x in dom f holds f.x is natural-valued Function; compatibility proof thus f is natural-functions-valued implies for x being object st x in dom f holds f.x is natural-valued Function proof assume A11: rng f is natural-functions-membered; let x; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A11; end; assume A12: for x being object st x in dom f holds f.x is natural-valued Function; let y be object; assume y in rng f; then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3; hence thesis by A12; end; end; registration cluster natural-functions-valued -> integer-functions-valued for Relation; coherence; cluster integer-functions-valued -> rational-functions-valued for Relation; coherence; cluster rational-functions-valued -> real-functions-valued for Relation; coherence; cluster real-functions-valued -> ext-real-functions-valued for Relation; coherence; cluster real-functions-valued -> complex-functions-valued for Relation; coherence; end; registration cluster empty -> natural-functions-valued for Relation; coherence; end; registration cluster natural-functions-valued for Function; existence proof take {}; thus thesis; end; end; registration let R be complex-functions-valued Relation; cluster rng R -> complex-functions-membered; coherence by Def20; end; registration let R be ext-real-functions-valued Relation; cluster rng R -> ext-real-functions-membered; coherence by Def21; end; registration let R be real-functions-valued Relation; cluster rng R -> real-functions-membered; coherence by Def22; end; registration let R be rational-functions-valued Relation; cluster rng R -> rational-functions-membered; coherence by Def23; end; registration let R be integer-functions-valued Relation; cluster rng R -> integer-functions-membered; coherence by Def24; end; registration let R be natural-functions-valued Relation; cluster rng R -> natural-functions-membered; coherence by Def25; end; registration let X; let Y be complex-functions-membered set; cluster -> complex-functions-valued for PartFunc of X,Y; coherence; end; registration let X; let Y be ext-real-functions-membered set; cluster -> ext-real-functions-valued for PartFunc of X,Y; coherence; end; registration let X; let Y be real-functions-membered set; cluster -> real-functions-valued for PartFunc of X,Y; coherence; end; registration let X; let Y be rational-functions-membered set; cluster -> rational-functions-valued for PartFunc of X,Y; coherence; end; registration let X; let Y be integer-functions-membered set; cluster -> integer-functions-valued for PartFunc of X,Y; coherence; end; registration let X; let Y be natural-functions-membered set; cluster -> natural-functions-valued for PartFunc of X,Y; coherence; end; registration cluster complex-functions-valued -> Function-yielding for Function; coherence proof let f be Function such that A1: f is complex-functions-valued; let x be object; thus thesis by A1; end; cluster real-functions-valued -> Function-yielding for Function; coherence; cluster ext-real-functions-valued -> Function-yielding for Function; coherence proof let f be Function such that A2: f is ext-real-functions-valued; let x be object; thus thesis by A2; end; end; registration let f be complex-functions-valued Function; let x be object; cluster f.x -> Function-like Relation-like; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be ext-real-functions-valued Function; let x be object; cluster f.x -> Function-like Relation-like; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be complex-functions-valued Function; let x be object; cluster f.x -> complex-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be ext-real-functions-valued Function; let x be object; cluster f.x -> ext-real-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be real-functions-valued Function; let x be object; cluster f.x -> real-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be rational-functions-valued Function; let x be object; cluster f.x -> RAT-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be integer-functions-valued Function; let x be object; cluster f.x -> INT-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be natural-functions-valued Function; let x be object; cluster f.x -> natural-valued; coherence proof per cases; suppose x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis; end; suppose not x in dom f; hence thesis by FUNCT_1:def 2; end; end; end; registration let f be real-functions-valued Function; let x,y; cluster f.(x,y) -> real-valued for Function; coherence; end; begin :: Operations reserve Y, Y1, Y2 for complex-functions-membered set, c, c1, c2 for Complex, f for PartFunc of X,Y, f1 for PartFunc of X1,Y1, f2 for PartFunc of X2, Y2, g, h, k for complex-valued Function; theorem Th7: g <> {} & g + c1 = g + c2 implies c1 = c2 proof assume that A1: g <> {} and A2: g+c1 = g+c2; consider x being object such that A3: x in dom g by A1,XBOOLE_0:def 1; dom g = dom(g+c2) by VALUED_1:def 2; then A4: (g+c2).x = g.x+c2 by A3,VALUED_1:def 2; dom g = dom(g+c1) by VALUED_1:def 2; then (g+c1).x = g.x+c1 by A3,VALUED_1:def 2; hence c1 = c2 by A2,A4; end; theorem Th8: g <> {} & g - c1 = g - c2 implies c1 = c2 proof assume that A1: g <> {} and A2: g-c1 = g-c2; consider x being object such that A3: x in dom g by A1,XBOOLE_0:def 1; dom g = dom(g-c2) by VALUED_1:def 2; then A4: (g-c2).x = g.x-c2 by A3,VALUED_1:def 2; dom g = dom(g-c1) by VALUED_1:def 2; then (g-c1).x = g.x-c1 by A3,VALUED_1:def 2; hence c1 = c2 by A2,A4; end; theorem Th9: g <> {} & g is non-empty & g (#) c1 = g (#) c2 implies c1 = c2 proof assume that A1: g <> {} and A2: g is non-empty and A3: g(#)c1 = g(#)c2; consider x being object such that A4: x in dom g by A1,XBOOLE_0:def 1; g.x in rng g by A4,FUNCT_1:def 3; then A5: g.x <> {} by A2,RELAT_1:def 9; (g(#)c1).x = g.x*c1 & (g(#)c2).x = g.x*c2 by VALUED_1:6; hence c1 = c2 by A3,A5,XCMPLX_1:5; end; theorem Th10: - (g + c) = -g - c proof A1: dom -(g+c) = dom(g+c) by VALUED_1:8; A2: dom(g+c) = dom g & dom(-g-c) = dom -g by VALUED_1:def 2; hence dom -(g+c) = dom(-g-c) by A1,VALUED_1:8; let x be object; assume A3: x in dom -(g+c); A4: dom -g = dom g by VALUED_1:8; thus (-(g+c)).x = -(g+c).x by VALUED_1:8 .= -(g.x+c) by A1,A3,VALUED_1:def 2 .= -g.x-c .= (-g).x-c by VALUED_1:8 .= (-g-c).x by A2,A1,A4,A3,VALUED_1:def 2; end; theorem Th11: - (g - c) = -g + c proof A1: dom -(g-c) = dom(g-c) by VALUED_1:8; A2: dom(g-c) = dom g & dom(-g+c) = dom -g by VALUED_1:def 2; hence dom -(g-c) = dom(-g+c) by A1,VALUED_1:8; let x be object; assume A3: x in dom -(g-c); A4: dom -g = dom g by VALUED_1:8; thus (-(g-c)).x = -(g-c).x by VALUED_1:8 .= -(g.x-c) by A1,A3,VALUED_1:def 2 .= -g.x+c .= (-g).x+c by VALUED_1:8 .= (-g+c).x by A2,A1,A4,A3,VALUED_1:def 2; end; theorem Th12: (g + c1) + c2 = g + (c1 + c2) proof A1: dom((g+c1)+c2) = dom(g+c1) by VALUED_1:def 2; A2: dom(g+c1) = dom g by VALUED_1:def 2; hence dom((g+c1)+c2) = dom(g+(c1+c2)) by A1,VALUED_1:def 2; let x be object; A3: dom(g+(c1+c2)) = dom(g) by VALUED_1:def 2; assume A4: x in dom((g+c1)+c2); hence ((g+c1)+c2).x = (g+c1).x+c2 by VALUED_1:def 2 .= g.x+c1+c2 by A1,A4,VALUED_1:def 2 .= g.x+(c1+c2) .= (g+(c1+c2)).x by A1,A2,A3,A4,VALUED_1:def 2; end; theorem Th13: (g + c1) - c2 = g + (c1 - c2) proof A1: dom((g+c1)-c2) = dom(g+c1) by VALUED_1:def 2; A2: dom(g+c1) = dom g by VALUED_1:def 2; hence dom((g+c1)-c2) = dom(g+(c1-c2)) by A1,VALUED_1:def 2; let x be object; A3: dom(g+(c1-c2)) = dom(g) by VALUED_1:def 2; assume A4: x in dom((g+c1)-c2); hence ((g+c1)-c2).x = (g+c1).x-c2 by VALUED_1:def 2 .= g.x+c1-c2 by A1,A4,VALUED_1:def 2 .= g.x+(c1-c2) .= (g+(c1-c2)).x by A1,A2,A3,A4,VALUED_1:def 2; end; theorem Th14: (g - c1) + c2 = g - (c1 - c2) proof A1: dom((g-c1)+c2) = dom(g-c1) by VALUED_1:def 2; A2: dom(g-c1) = dom g by VALUED_1:def 2; hence dom((g-c1)+c2) = dom(g-(c1-c2)) by A1,VALUED_1:def 2; let x be object; A3: dom(g-(c1-c2)) = dom(g) by VALUED_1:def 2; assume A4: x in dom((g-c1)+c2); hence ((g-c1)+c2).x = (g-c1).x+c2 by VALUED_1:def 2 .= g.x-c1+c2 by A1,A4,VALUED_1:def 2 .= g.x-(c1-c2) .= (g-(c1-c2)).x by A1,A2,A3,A4,VALUED_1:def 2; end; theorem Th15: (g - c1) - c2 = g - (c1 + c2) proof A1: dom((g-c1)-c2) = dom(g-c1) by VALUED_1:def 2; A2: dom(g-c1) = dom g by VALUED_1:def 2; hence dom((g-c1)-c2) = dom(g-(c1+c2)) by A1,VALUED_1:def 2; let x be object; A3: dom(g-(c1+c2)) = dom(g) by VALUED_1:def 2; assume A4: x in dom((g-c1)-c2); hence ((g-c1)-c2).x = (g-c1).x-c2 by VALUED_1:def 2 .= g.x-c1-c2 by A1,A4,VALUED_1:def 2 .= g.x-(c1+c2) .= (g-(c1+c2)).x by A1,A2,A3,A4,VALUED_1:def 2; end; theorem Th16: g (#) c1 (#) c2 = g (#) (c1 * c2) proof dom((g(#)c1)(#)c2) = dom(g(#)c1) & dom(g(#)c1) = dom g by VALUED_1:def 5; hence dom((g(#)c1)(#)c2) = dom(g(#)(c1*c2)) by VALUED_1:def 5; let x be object; assume x in dom((g(#)c1)(#)c2); thus ((g(#)c1)(#)c2).x = (g(#)c1).x*c2 by VALUED_1:6 .= g.x*c1*c2 by VALUED_1:6 .= g.x*(c1*c2) .= (g(#)(c1*c2)).x by VALUED_1:6; end; theorem Th17: - (g + h) = (-g) - h proof A1: dom -(g+h) = dom(g+h) by VALUED_1:8; dom(g+h) = dom g /\ dom h & dom(-g-h) = dom(-g) /\ dom h by VALUED_1:12,def 1 ; hence A2: dom -(g+h) = dom(-g-h) by A1,VALUED_1:8; let x be object; assume A3: x in dom -(g+h); thus (-(g+h)).x = -(g+h).x by VALUED_1:8 .= -(g.x+h.x) by A1,A3,VALUED_1:def 1 .= -g.x-h.x .= (-g).x-h.x by VALUED_1:8 .= (-g-h).x by A2,A3,VALUED_1:13; end; theorem Th18: g - h = - (h - g) proof A1: dom -(h-g) = dom(h-g) by VALUED_1:8; dom(g-h) = dom g /\ dom h by VALUED_1:12; hence A2: dom(g-h) = dom -(h-g) by A1,VALUED_1:12; let x be object; assume A3: x in dom(g-h); hence (g-h).x = g.x-h.x by VALUED_1:13 .= -(h.x-g.x) .= -(h-g).x by A1,A2,A3,VALUED_1:13 .= (-(h-g)).x by VALUED_1:8; end; theorem Th19: g (#) h /" k = g (#) (h /" k) proof A1: dom(g (#) (h /" k)) = dom g /\ dom(h /" k) & dom(g (#) h /" k) = dom(g (#) h ) /\ dom k by VALUED_1:16,def 4; dom(g (#) h) = dom g /\ dom h & dom(h /" k) = dom h /\ dom k by VALUED_1:16 ,def 4; hence dom(g (#) h /" k) = dom(g (#) (h /" k)) by A1,XBOOLE_1:16; let x be object; assume x in dom(g (#) h /" k); thus (g (#) h /" k).x = (g (#) h).x / k.x by VALUED_1:17 .= g.x * h.x / k.x by VALUED_1:5 .= g.x * (h.x / k.x) .= g.x * (h /" k).x by VALUED_1:17 .= (g (#) (h /" k)).x by VALUED_1:5; end; theorem Th20: g /" h (#) k = g (#) k /" h proof A1: dom(g /" h (#) k) = dom(g /" h) /\ dom k & dom(g (#) k /" h) = dom(g (#) k) /\ dom h by VALUED_1:16,def 4; dom(g /" h) = dom g /\ dom h & dom(g (#) k) = dom g /\ dom k by VALUED_1:16 ,def 4; hence dom(g /" h (#) k) = dom(g (#) k /" h) by A1,XBOOLE_1:16; let x be object; assume x in dom(g /" h (#) k); thus (g /" h (#) k).x = (g /" h).x * k.x by VALUED_1:5 .= g.x / h.x * k.x by VALUED_1:17 .= g.x * k.x / h.x .= (g(#)k).x / h.x by VALUED_1:5 .= (g (#) k /" h).x by VALUED_1:17; end; theorem Th21: g /" h /" k = g /" (h (#) k) proof A1: dom(g /" h /" k) = dom(g /" h) /\ dom k & dom(g /" (h (#) k)) = dom g /\ dom (h (#) k) by VALUED_1:16; dom(g /" h) = dom g /\ dom h & dom(h (#) k) = dom h /\ dom k by VALUED_1:16 ,def 4; hence dom(g /" h /" k) = dom(g /" (h (#) k)) by A1,XBOOLE_1:16; let x be object; assume x in dom(g /" h /" k); thus (g /" h /" k).x = (g /" h).x / k.x by VALUED_1:17 .= g.x / h.x / k.x by VALUED_1:17 .= g.x / (h.x * k.x) by XCMPLX_1:78 .= g.x / (h (#) k).x by VALUED_1:5 .= (g /" (h (#) k)).x by VALUED_1:17; end; theorem Th22: c(#)-g = (-c)(#)g proof dom(c(#)-g) = dom -g by VALUED_1:def 5 .= dom g by VALUED_1:8; hence dom(c(#)-g) = dom((-c)(#)g) by VALUED_1:def 5; let x be object; assume x in dom(c(#)-g); thus (c(#)-g).x = c*((-g).x) by VALUED_1:6 .= c*(-g.x) by VALUED_1:8 .= (-c)*g.x .= ((-c)(#)g).x by VALUED_1:6; end; theorem Th23: c(#)-g = -(c(#)g) proof A1: dom(-(c(#)g)) = dom(c(#)g) by VALUED_1:8 .= dom g by VALUED_1:def 5; dom(c(#)-g) = dom -g by VALUED_1:def 5 .= dom g by VALUED_1:8; hence dom(c(#)-g) = dom -(c(#)g) by A1; let x be object; assume x in dom(c(#)-g); thus (c(#)-g).x = c*((-g).x) by VALUED_1:6 .= c*(-g.x) by VALUED_1:8 .= -(c*g.x) .= -(c(#)g).x by VALUED_1:6 .= (-(c(#)g)).x by VALUED_1:8; end; theorem Th24: (-c)(#)g = -(c(#)g) proof thus (-c)(#)g = c(#)-g by Th22 .= -(c(#)g) by Th23; end; theorem Th25: - (g (#) h) = (-g) (#) h proof A1: dom -(g(#)h) = dom(g(#)h) by VALUED_1:8; dom(g(#)h) = dom g /\ dom h & dom((-g)(#)h) = dom(-g) /\ dom h by VALUED_1:def 4; hence dom -(g(#)h) = dom((-g)(#)h) by A1,VALUED_1:8; let x be object; assume x in dom -(g(#)h); thus (-(g(#)h)).x = -(g(#)h).x by VALUED_1:8 .= -(g.x*h.x) by VALUED_1:5 .= (-g.x)*h.x .= (-g).x*h.x by VALUED_1:8 .= ((-g)(#)h).x by VALUED_1:5; end; theorem - (g /" h) = (-g) /" h proof A1: dom -(g/"h) = dom(g/"h) by VALUED_1:8; dom(g/"h) = dom g /\ dom h & dom((-g)/"h) = dom(-g) /\ dom h by VALUED_1:16; hence dom -(g/"h) = dom((-g)/"h) by A1,VALUED_1:8; let x be object; assume x in dom -(g/"h); thus (-(g/"h)).x = -(g/"h).x by VALUED_1:8 .= -(g.x/h.x) by VALUED_1:17 .= (-g.x)/h.x .= (-g).x/h.x by VALUED_1:8 .= ((-g)/"h).x by VALUED_1:17; end; theorem Th27: - (g /" h) = g /" -h proof A1: dom -h = dom h by VALUED_1:8; dom(g/"h) = dom g /\ dom h & dom(g/"-h) = dom g /\ dom -h by VALUED_1:16; hence dom -(g/"h) = dom(g/"-h) by A1,VALUED_1:8; let x be object; assume x in dom -(g/"h); thus (-(g/"h)).x = -(g/"h).x by VALUED_1:8 .= -(g.x/h.x) by VALUED_1:17 .= g.x/-h.x by XCMPLX_1:188 .= g.x/(-h).x by VALUED_1:8 .= (g/"-h).x by VALUED_1:17; end; definition let f be complex-valued Function, c be Complex; func f (/) c -> Function equals (1/c) (#) f; coherence; end; registration let f be complex-valued Function, c be Complex; cluster f (/) c -> complex-valued; coherence; end; registration let f be real-valued Function, r be Real; cluster f (/) r -> real-valued; coherence; end; registration let f be RAT-valued Function, r be Rational; cluster f (/) r -> RAT-valued; coherence; end; registration let f be complex-valued FinSequence, c be Complex; cluster f (/) c -> FinSequence-like; coherence; end; theorem dom(g(/)c) = dom g by VALUED_1:def 5; theorem for x being object holds (g(/)c).x = g.x / c by VALUED_1:6; theorem Th30: (-g) (/) c = -(g(/)c) proof thus (-g) (/) c = (-(1/c)) (#) g by Th22 .= -(g(/)c) by Th24; end; theorem Th31: g (/) -c = -(g(/)c) proof thus g (/) -c = (-1/c) (#) g by XCMPLX_1:188 .= -(g(/)c) by Th24; end; theorem g (/) -c = (-g) (/) c proof thus g (/) -c = - (g(/)c) by Th31 .= (-g) (/) c by Th30; end; theorem Th33: g <> {} & g is non-empty & g (/) c1 = g (/) c2 implies c1 = c2 proof assume that A1: g <> {} and A2: g is non-empty and A3: g(/)c1 = g(/)c2; consider x being object such that A4: x in dom g by A1,XBOOLE_0:def 1; g.x in rng g by A4,FUNCT_1:def 3; then A5: g.x <> {} by A2,RELAT_1:def 9; (g(/)c1).x = g.x/c1 & (g(/)c2).x = g.x/c2 by VALUED_1:6; then c1" = c2" by A3,A5,XCMPLX_1:5; hence c1 = c2 by XCMPLX_1:201; end; theorem g (#) c1 (/) c2 = g (#) (c1 / c2) proof dom(g(#)c1) = dom g & dom(g(#)c1(/)c2) = dom(g(#)c1) by VALUED_1:def 5; hence dom(g(#)c1(/)c2) = dom(g(#)(c1/c2)) by VALUED_1:def 5; let x be object; assume x in dom(g(#)c1(/)c2); thus (g(#)c1(/)c2).x = (g(#)c1).x * c2" by VALUED_1:6 .= g.x * c1 * c2" by VALUED_1:6 .= g.x*(c1/c2) .= (g(#)(c1/c2)).x by VALUED_1:6; end; theorem g (/) c1 (#) c2 = g (#) c2 (/) c1 proof A1: dom(g(/)c1(#)c2) = dom(g(/)c1) by VALUED_1:def 5; dom(g(/)c1) = dom g & dom(g(#)c2) = dom g by VALUED_1:def 5; hence dom(g(/)c1(#)c2) = dom(g(#)c2(/)c1) by A1,VALUED_1:def 5; let x be object; assume x in dom(g(/)c1(#)c2); thus (g(/)c1(#)c2).x = (g(/)c1).x * c2 by VALUED_1:6 .= g.x * c1" * c2 by VALUED_1:6 .= (g.x*c2)*c1" .= (g(#)c2).x*c1" by VALUED_1:6 .= (g(#)c2(/)c1).x by VALUED_1:6; end; theorem g (/) c1 (/) c2 = g (/) (c1*c2) proof dom(g(/)c1) = dom g & dom(g(/)(c1*c2)) = dom g by VALUED_1:def 5; hence dom(g(/)c1(/)c2) = dom(g(/)(c1*c2)) by VALUED_1:def 5; let x be object; assume x in dom(g(/)c1(/)c2); thus (g(/)c1(/)c2).x = (g(/)c1).x * c2" by VALUED_1:6 .= g.x * c1" * c2" by VALUED_1:6 .= g.x * (c1" * c2") .= g.x * (c1*c2)" by XCMPLX_1:204 .= (g(/)(c1*c2)).x by VALUED_1:6; end; theorem (g+h) (/) c = g(/)c + h(/)c proof A1: dom((g+h)(/)c) = dom(g+h) by VALUED_1:def 5; A2: dom(g+h) = dom g /\ dom h by VALUED_1:def 1; dom(g(/)c) = dom g & dom(h(/)c) = dom h by VALUED_1:def 5; hence A3: dom((g+h)(/)c) = dom(g(/)c+h(/)c) by A1,A2,VALUED_1:def 1; let x be object; assume A4: x in dom((g+h)(/)c); thus ((g+h)(/)c).x = (g+h).x * c" by VALUED_1:6 .= (g.x+h.x)*c" by A1,A4,VALUED_1:def 1 .= g.x*c" + h.x*c" .= (g(/)c).x + h.x*c" by VALUED_1:6 .= (g(/)c).x + (h(/)c).x by VALUED_1:6 .= (g(/)c+h(/)c).x by A3,A4,VALUED_1:def 1; end; theorem (g-h) (/) c = g(/)c - h(/)c proof A1: dom((g-h)(/)c) = dom(g-h) by VALUED_1:def 5; A2: dom(g-h) = dom g /\ dom h by VALUED_1:12; dom(g(/)c) = dom g & dom(h(/)c) = dom h by VALUED_1:def 5; hence A3: dom((g-h)(/)c) = dom(g(/)c-h(/)c) by A1,A2,VALUED_1:12; let x be object; assume A4: x in dom((g-h)(/)c); thus ((g-h)(/)c).x = (g-h).x * c" by VALUED_1:6 .= (g.x-h.x)*c" by A1,A4,VALUED_1:13 .= g.x*c" - h.x*c" .= (g(/)c).x - h.x*c" by VALUED_1:6 .= (g(/)c).x - (h(/)c).x by VALUED_1:6 .= (g(/)c-h(/)c).x by A3,A4,VALUED_1:13; end; theorem (g(#)h) (/) c = g (#) (h(/)c) proof A1: dom((g(#)h)(/)c) = dom(g(#)h) by VALUED_1:def 5; dom(g(#)h) = dom g /\ dom h & dom(h(/)c) = dom h by VALUED_1:def 4,def 5; hence dom((g(#)h)(/)c) = dom(g(#)(h(/)c)) by A1,VALUED_1:def 4; let x be object; assume x in dom((g(#)h)(/)c); thus ((g(#)h)(/)c).x = (g(#)h).x * c" by VALUED_1:6 .= g.x*h.x*c" by VALUED_1:5 .= g.x*(h.x*c") .= g.x * (h(/)c).x by VALUED_1:6 .= (g(#)(h(/)c)).x by VALUED_1:5; end; theorem (g/"h) (/) c = g /" (h(#)c) proof A1: dom((g/"h)(/)c) = dom(g/"h) by VALUED_1:def 5; dom(g/"h) = dom g /\ dom h & dom(h(#)c) = dom h by VALUED_1:16,def 5; hence dom((g/"h)(/)c) = dom(g/"(h(#)c)) by A1,VALUED_1:16; let x be object; assume x in dom((g/"h)(/)c); thus ((g/"h)(/)c).x = (g/"h).x * c" by VALUED_1:6 .= g.x/h.x/c by VALUED_1:17 .= g.x/(h.x*c) by XCMPLX_1:78 .= g.x / (h(#)c).x by VALUED_1:6 .= (g/"(h(#)c)).x by VALUED_1:17; end; definition let f be complex-functions-valued Function; deffunc F(object) = -f.\$1; func <->f -> Function means :Def33: dom it = dom f & for x being object st x in dom it holds it.x = -f.x; existence proof ex F being Function st dom F = dom f & for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; redefine func <->f -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof set h = <->f; A1: dom h = dom f by Def33; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = -f.x by A2,Def33; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:8; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; redefine func <->f -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof set h = <->f; A1: dom h = dom f by Def33; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = -f.x by A2,Def33; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:8; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; redefine func <->f -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof set h = <->f; A1: dom h = dom f by Def33; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = -f.x by A2,Def33; A5: rng y c= RAT by A3,A4,RAT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:8; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; redefine func <->f -> PartFunc of X, I_PFuncs(DOMS(Y)); coherence proof set h = <->f; A1: dom h = dom f by Def33; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = -f.x by A2,Def33; A5: rng y c= INT by A3,A4,INT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:8; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; registration let Y be complex-functions-membered set; let f be FinSequence of Y; cluster <->f -> FinSequence-like; coherence proof dom<->f = dom f & ex n being Nat st dom f = Seg n by Def33,FINSEQ_1:def 2; hence thesis by FINSEQ_1:def 2; end; end; theorem <-><->f = f proof set f1 = <->f; A1: dom f1 = dom f by Def33; hence A2: dom<->f1 = dom f by Def33; let x be object; assume A3: x in dom<->f1; hence (<->f1).x = -f1.x by Def33 .= -(-f.x) by A1,A2,A3,Def33 .= f.x; end; theorem <->f1 = <->f2 implies f1 = f2 proof A1: dom <->f1 = dom f1 by Def33; assume A2: <->f1 = <->f2; hence dom f1 = dom f2 by A1,Def33; let x be object; assume A3: x in dom f1; thus f1.x = --f1.x .= -(<->f1).x by A1,A3,Def33 .= --f2.x by A2,A1,A3,Def33 .= f2.x; end; definition let X be complex-functions-membered set; let Y be set; let f be PartFunc of X,Y; defpred P[object,object] means ex a being complex-valued Function st \$1 = a & \$2 = f.-a; func f(-) -> Function means dom it = dom f & for x being complex-valued Function st x in dom it holds it.x = f.-x; existence proof A1: for x being object st x in dom f ex y being object st P[x,y] proof let x be object; assume x in dom f; then reconsider a = x as complex-valued Function; take f.-a, a; thus thesis; end; consider F being Function such that A2: dom F = dom f and A3: for x being object st x in dom f holds P[x,F.x] from CLASSES1:sch 1( A1); take F; thus dom F = dom f by A2; let x be complex-valued Function; assume x in dom F; then P[x,F.x] by A2,A3; hence thesis; end; uniqueness proof let F, G be Function such that A4: dom F = dom f and A5: for x being complex-valued Function st x in dom F holds F.x = f.- x and A6: dom G = dom f and A7: for x being complex-valued Function st x in dom G holds G.x = f.- x; thus dom F = dom G by A4,A6; let x be object; assume A8: x in dom F; then reconsider y = x as complex-valued Function by A4; thus F.x = f.-y by A5,A8 .= G.x by A4,A6,A7,A8; end; end; definition let f be complex-functions-valued Function; deffunc F(object) = (f.\$1)"; func f -> Function means :Def35: dom it = dom f & for x being object st x in dom it holds it.x = (f.x)"; existence proof ex F being Function st dom F = dom f & for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; redefine func f -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof set h = f; A1: dom h = dom f by Def35; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = (f.x)" by A2,Def35; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 7; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; redefine func f -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof set h = f; A1: dom h = dom f by Def35; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = (f.x)" by A2,Def35; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 7; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; redefine func f -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof set h = f; A1: dom h = dom f by Def35; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = (f.x)" by A2,Def35; A5: rng y c= RAT by A3,A4,RAT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 7; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; registration let Y be complex-functions-membered set; let f be FinSequence of Y; cluster f -> FinSequence-like; coherence proof dom f = dom f & ex n being Nat st dom f = Seg n by Def35,FINSEQ_1:def 2; hence thesis by FINSEQ_1:def 2; end; end; theorem f = f proof set f1 = f; A1: dom f1 = dom f by Def35; hence A2: dom f1 = dom f by Def35; let x be object; assume A3: x in dom f1; hence (f1).x = (f1.x)" by Def35 .= (f.x)"" by A1,A2,A3,Def35 .= f.x; end; definition let f be complex-functions-valued Function; deffunc F(object) = abs(f.\$1); func abs(f) -> Function means :Def36: dom it = dom f & for x being object st x in dom it holds it.x = abs(f.x); existence proof ex F being Function st dom F = dom f & for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; redefine func abs(f) -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof set h = abs(f); A1: dom h = dom f by Def36; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = abs(f.x) by A2,Def36; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 11; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; redefine func abs(f) -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof set h = abs(f); A1: dom h = dom f by Def36; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = abs(f.x) by A2,Def36; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 11; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; redefine func abs(f) -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof set h = abs(f); A1: dom h = dom f by Def36; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = abs(f.x) by A2,Def36; A5: rng y c= RAT by A3,A4,RAT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 11; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; redefine func abs(f) -> PartFunc of X, N_PFuncs(DOMS(Y)); coherence proof set h = abs(f); A1: dom h = dom f by Def36; rng h c= N_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = abs(f.x) by A2,Def36; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 11; then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; registration let Y be complex-functions-membered set; let f be FinSequence of Y; cluster abs(f) -> FinSequence-like; coherence proof dom abs(f) = dom f & ex n being Nat st dom f = Seg n by Def36, FINSEQ_1:def 2; hence thesis by FINSEQ_1:def 2; end; end; theorem abs abs f = abs f proof set f1 = abs f; thus A1: dom abs f1 = dom abs f by Def36; let x be object; assume A2: x in dom abs f1; hence (abs f1).x = abs(f1.x) by Def36 .= abs(abs(f.x)) by A1,A2,Def36 .= (abs f).x by A1,A2,Def36; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let c be Complex; deffunc F(object) = c+(f.\$1); func f[+]c -> Function means :Def37: dom it = dom f & for x being object st x in dom it holds it.x = c + f.x; existence proof ex F being Function st dom F = dom f & for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let c be Complex; redefine func f[+]c -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof set h = f[+]c; A1: dom h = dom f by Def37; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x + c by A2,Def37; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let c be Real; redefine func f[+]c -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof set h = f[+]c; A1: dom h = dom f by Def37; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + c by A2,Def37; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let c be Rational; redefine func f[+]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof set h = f[+]c; A1: dom h = dom f by Def37; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + c by A2,Def37; A5: rng y c= RAT by A3,A4,RAT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let c be Integer; redefine func f[+]c -> PartFunc of X, I_PFuncs(DOMS(Y)); coherence proof set h = f[+]c; A1: dom h = dom f by Def37; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + c by A2,Def37; A5: rng y c= INT by A3,A4,INT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be natural-functions-membered set; let f be PartFunc of X,Y; let c be Nat; redefine func f[+]c -> PartFunc of X, N_PFuncs(DOMS(Y)); coherence proof set h = f[+]c; A1: dom h = dom f by Def37; rng h c= N_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + c by A2,Def37; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem f [+] c1 [+] c2 = f [+] (c1+c2) proof set f1 = f[+]c1; A1: dom(f1[+]c2) = dom f1 by Def37; dom f1 = dom f by Def37; hence A2: dom(f1[+]c2) = dom(f[+](c1+c2)) by A1,Def37; let x be object; assume A3: x in dom(f1[+]c2); hence (f1[+]c2).x = f1.x + c2 by Def37 .= f.x + c1 + c2 by A1,A3,Def37 .= f.x + (c1 + c2) by Th12 .= (f[+](c1+c2)).x by A2,A3,Def37; end; theorem f <> {} & f is non-empty & f [+] c1 = f [+] c2 implies c1 = c2 proof assume that A1: f <> {} and A2: f is non-empty and A3: f[+]c1 = f[+]c2; consider x being object such that A4: x in dom f by A1,XBOOLE_0:def 1; f.x in rng f by A4,FUNCT_1:def 3; then A5: f.x <> {} by A2,RELAT_1:def 9; dom f = dom(f[+]c2) by Def37; then A6: (f[+]c2).x = f.x+c2 by A4,Def37; dom f = dom(f[+]c1) by Def37; then (f[+]c1).x = f.x+c1 by A4,Def37; hence c1 = c2 by A3,A5,A6,Th7; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let c be Complex; func f[-]c -> Function equals f [+] -c; coherence; end; theorem dom(f[-]c) = dom f by Def37; theorem x in dom(f[-]c) implies (f[-]c).x = f.x - c by Def37; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let c be Complex; redefine func f[-]c -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof f[-]c = f [+] -c; hence thesis; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let c be Real; redefine func f[-]c -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof f[-]c = f [+] -c; hence thesis; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let c be Rational; redefine func f[-]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof f[-]c = f [+] -c; hence thesis; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let c be Integer; redefine func f[-]c -> PartFunc of X, I_PFuncs(DOMS(Y)); coherence proof f[-]c = f [+] -c; hence thesis; end; end; theorem f <> {} & f is non-empty & f [-] c1 = f [-] c2 implies c1 = c2 proof assume that A1: f <> {} and A2: f is non-empty and A3: f[-]c1 = f[-]c2; consider x being object such that A4: x in dom f by A1,XBOOLE_0:def 1; f.x in rng f by A4,FUNCT_1:def 3; then A5: f.x <> {} by A2,RELAT_1:def 9; dom f = dom(f[-]c2) by Def37; then A6: (f[-]c2).x = f.x-c2 by A4,Def37; dom f = dom(f[-]c1) by Def37; then (f[-]c1).x = f.x-c1 by A4,Def37; hence c1 = c2 by A3,A5,A6,Th8; end; theorem f [+] c1 [-] c2 = f [+] (c1-c2) proof set f1 = f[+]c1; A1: dom(f1[-]c2) = dom f1 by Def37; dom f1 = dom f by Def37; hence A2: dom(f1[-]c2) = dom(f[+](c1-c2)) by A1,Def37; let x be object; assume A3: x in dom(f1[-]c2); hence (f1[-]c2).x = f1.x - c2 by Def37 .= f.x + c1 - c2 by A1,A3,Def37 .= f.x + (c1 - c2) by Th12 .= (f[+](c1-c2)).x by A2,A3,Def37; end; theorem f [-] c1 [+] c2 = f [-] (c1-c2) proof set f1 = f[-]c1; A1: dom(f1[+]c2) = dom f1 by Def37; dom f1 = dom f by Def37; hence A2: dom(f1[+]c2) = dom(f[-](c1-c2)) by A1,Def37; let x be object; assume A3: x in dom(f1[+]c2); hence (f1[+]c2).x = f1.x + c2 by Def37 .= f.x - c1 + c2 by A1,A3,Def37 .= f.x - (c1 - c2) by Th14 .= (f[-](c1-c2)).x by A2,A3,Def37; end; theorem f [-] c1 [-] c2 = f [-] (c1+c2) proof set f1 = f[-]c1; A1: dom(f1[-]c2) = dom f1 by Def37; dom f1 = dom f by Def37; hence A2: dom(f1[-]c2) = dom(f[-](c1+c2)) by A1,Def37; let x be object; assume A3: x in dom(f1[-]c2); hence (f1[-]c2).x = f1.x - c2 by Def37 .= f.x - c1 - c2 by A1,A3,Def37 .= f.x - (c1 + c2) by Th15 .= (f[-](c1+c2)).x by A2,A3,Def37; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let c be Complex; deffunc F(object) = c(#)(f.\$1); func f[#]c -> Function means :Def39: dom it = dom f & for x being object st x in dom it holds it.x = c (#) (f.x); existence proof ex F being Function st dom F = dom f & for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let c be Complex; redefine func f[#]c -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof set h = f[#]c; A1: dom h = dom f by Def39; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = c (#) f.x by A2,Def39; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let c be Real; redefine func f[#]c -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof set h = f[#]c; A1: dom h = dom f by Def39; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = c (#) f.x by A2,Def39; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let c be Rational; redefine func f[#]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof set h = f[#]c; A1: dom h = dom f by Def39; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = c (#) f.x by A2,Def39; A5: rng y c= RAT by A3,A4,RAT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let c be Integer; redefine func f[#]c -> PartFunc of X, I_PFuncs(DOMS(Y)); coherence proof set h = f[#]c; A1: dom h = dom f by Def39; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = c (#) f.x by A2,Def39; A5: rng y c= INT by A3,A4,INT_1:def 2; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be natural-functions-membered set; let f be PartFunc of X,Y; let c be Nat; redefine func f[#]c -> PartFunc of X, N_PFuncs(DOMS(Y)); coherence proof set h = f[#]c; A1: dom h = dom f by Def39; rng h c= N_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = c (#) f.x by A2,Def39; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; f.x in Y by A1,A2,PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem f [#] c1 [#] c2 = f [#] (c1*c2) proof set f1 = f[#]c1; A1: dom(f1[#]c2) = dom f1 by Def39; dom f1 = dom f by Def39; hence A2: dom(f1[#]c2) = dom(f[#](c1*c2)) by A1,Def39; let x be object; assume A3: x in dom(f1[#]c2); hence (f1[#]c2).x = f1.x (#) c2 by Def39 .= f.x (#) c1 (#) c2 by A1,A3,Def39 .= f.x (#) (c1 * c2) by Th16 .= (f[#](c1*c2)).x by A2,A3,Def39; end; theorem f <> {} & f is non-empty & (for x st x in dom f holds f.x is non-empty ) & f [#] c1 = f [#] c2 implies c1 = c2 proof assume that A1: f <> {} and A2: f is non-empty and A3: for x st x in dom f holds f.x is non-empty and A4: f[#]c1 = f[#]c2; consider x being object such that A5: x in dom f by A1,XBOOLE_0:def 1; dom f = dom(f[#]c2) by Def39; then A6: (f[#]c2).x = f.x(#)c2 by A5,Def39; dom f = dom(f[#]c1) by Def39; then A7: (f[#]c1).x = f.x(#)c1 by A5,Def39; f.x in rng f by A5,FUNCT_1:def 3; then A8: f.x <> {} by A2,RELAT_1:def 9; f.x is non-empty by A3,A5; hence c1 = c2 by A4,A8,A7,A6,Th9; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let c be Complex; func f[/]c -> Function equals f [#] (c"); coherence; end; theorem dom(f[/]c) = dom f by Def39; theorem x in dom(f[/]c) implies (f[/]c).x = c" (#) f.x by Def39; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let c be Complex; redefine func f[/]c -> PartFunc of X, C_PFuncs(DOMS(Y)); coherence proof f[/]c = f [#] (c"); hence thesis; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let c be Real; redefine func f[/]c -> PartFunc of X, R_PFuncs(DOMS(Y)); coherence proof f[/]c = f [#] (c"); hence thesis; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let c be Rational; redefine func f[/]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); coherence proof f[/]c = f [#] (c"); hence thesis; end; end; theorem f [/] c1 [/] c2 = f [/] (c1*c2) proof set f1 = f[/]c1; A1: dom(f1[/]c2) = dom f1 by Def39; dom f1 = dom f by Def39; hence A2: dom(f1[/]c2) = dom(f[/](c1*c2)) by A1,Def39; let x be object; assume A3: x in dom(f1[/]c2); hence (f1[/]c2).x = f1.x (#) c2" by Def39 .= f.x (#) c1" (#) c2" by A1,A3,Def39 .= f.x (#) (c1" * c2") by Th16 .= f.x (#) (c1*c2)" by XCMPLX_1:204 .= (f[/](c1*c2)).x by A2,A3,Def39; end; theorem f <> {} & f is non-empty & (for x st x in dom f holds f.x is non-empty ) & f [/] c1 = f [/] c2 implies c1 = c2 proof assume that A1: f <> {} and A2: f is non-empty and A3: for x st x in dom f holds f.x is non-empty and A4: f[/]c1 = f[/]c2; consider x being object such that A5: x in dom f by A1,XBOOLE_0:def 1; dom f = dom(f[/]c2) by Def39; then A6: (f[/]c2).x = f.x(/)c2 by A5,Def39; dom f = dom(f[/]c1) by Def39; then A7: (f[/]c1).x = f.x(/)c1 by A5,Def39; f.x in rng f by A5,FUNCT_1:def 3; then A8: f.x <> {} by A2,RELAT_1:def 9; f.x is non-empty by A3,A5; hence c1 = c2 by A4,A8,A7,A6,Th33; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let g be complex-valued Function; deffunc F(object) = f.\$1+g.\$1; func f<+>g -> Function means :Def41: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x + g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let g be complex-valued Function; redefine func f<+>g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); coherence proof set h = f<+>g; A1: dom h = dom f /\ dom g by Def41; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x + g.x by A2,Def41; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let g be real-valued Function; redefine func f<+>g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); coherence proof set h = f<+>g; A1: dom h = dom f /\ dom g by Def41; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def41; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let g be RAT-valued Function; redefine func f<+>g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); coherence proof set h = f<+>g; A1: dom h = dom f /\ dom g by Def41; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def41; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let g be INT-valued Function; redefine func f<+>g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); coherence proof set h = f<+>g; A1: dom h = dom f /\ dom g by Def41; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def41; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be natural-functions-membered set; let f be PartFunc of X,Y; let g be natural-valued Function; redefine func f<+>g -> PartFunc of X /\ dom g, N_PFuncs(DOMS(Y)); coherence proof set h = f<+>g; A1: dom h = dom f /\ dom g by Def41; rng h c= N_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def41; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem f <+> g <+> h = f <+> (g+h) proof set f1 = f<+>g; A1: dom(g+h) = dom g /\ dom h by VALUED_1:def 1; A2: dom(f1<+>h) = dom f1 /\ dom h by Def41; dom f1 = dom f /\ dom g & dom(f<+>(g+h)) = dom f /\ dom(g+h) by Def41; hence A3: dom(f1<+>h) = dom(f<+>(g+h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1<+>h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; A6: x in dom(g+h) by A3,A4,XBOOLE_0:def 4; thus (f1<+>h).x = f1.x + h.x by A4,Def41 .= f.x + g.x + h.x by A5,Def41 .= f.x + (g.x + h.x) by Th12 .= f.x + ((g+h).x) by A6,VALUED_1:def 1 .= (f<+>(g+h)).x by A3,A4,Def41; end; theorem <->(f<+>g) = (<->f) <+> -g proof set f1 = f<+>g, f2 = <->f; A1: dom <->f1 = dom f1 by Def33; A2: dom f1 = dom f /\ dom g & dom f2 = dom f by Def33,Def41; dom -g = dom g by VALUED_1:8; hence A3: dom <->f1 = dom(f2<+>-g) by A1,A2,Def41; let x be object; assume A4: x in dom <->f1; then A5: x in dom f2 by A1,A2,XBOOLE_0:def 4; thus (<->f1).x = -f1.x by A4,Def33 .= -(f.x+g.x) by A1,A4,Def41 .= -f.x-g.x by Th10 .= -f.x+(-g).x by VALUED_1:8 .= f2.x+(-g).x by A5,Def33 .= (f2<+>-g).x by A3,A4,Def41; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let g be complex-valued Function; func f<->g -> Function equals f <+> -g; coherence; end; theorem Th61: dom(f<->g) = dom f /\ dom g proof thus dom(f<->g) = dom f /\ dom -g by Def41 .= dom f /\ dom g by VALUED_1:8; end; theorem Th62: x in dom(f<->g) implies (f<->g).x = f.x - g.x proof assume x in dom(f<->g); hence (f<->g).x = f.x + (-g).x by Def41 .= f.x - g.x by VALUED_1:8; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let g be complex-valued Function; redefine func f<->g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); coherence proof set h = f<->g; A1: dom h = dom f /\ dom g by Th61; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x - g.x by A2,Th62; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; h.x = f.x - g.x by A2,Th62; then dom y = dom(f.x) by A3,VALUED_1:def 2; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let g be real-valued Function; redefine func f<->g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); coherence proof set h = f<->g; A1: dom h = dom f /\ dom g by Th61; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Th62; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let g be RAT-valued Function; redefine func f<->g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); coherence proof set h = f<->g; A1: dom h = dom f /\ dom g by Th61; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Th62; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let g be INT-valued Function; redefine func f<->g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); coherence proof set h = f<->g; A1: dom h = dom f /\ dom g by Th61; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Th62; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 2; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; theorem f <-> -g = f <+> g; theorem <->(f<->g) = (<->f) <+> g proof set f1 = f<->g, f2 = <->f; A1: dom <->f1 = dom f1 by Def33; A2: dom f1 = dom f /\ dom g & dom f2 = dom f by Def33,Th61; hence A3: dom <->f1 = dom(f2<+>g) by A1,Def41; let x be object; assume A4: x in dom <->f1; then A5: x in dom f2 by A1,A2,XBOOLE_0:def 4; thus (<->f1).x = -f1.x by A4,Def33 .= -(f.x-g.x) by A1,A4,Th62 .= -f.x+g.x by Th11 .= f2.x+g.x by A5,Def33 .= (f2<+>g).x by A3,A4,Def41; end; theorem f <+> g <-> h = f <+> (g-h) proof set f1 = f<+>g; A1: dom(g-h) = dom g /\ dom h by VALUED_1:12; A2: dom(f1<->h) = dom f1 /\ dom h by Th61; dom f1 = dom f /\ dom g & dom(f<+>(g-h)) = dom f /\ dom(g-h) by Def41; hence A3: dom(f1<->h) = dom(f<+>(g-h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1<->h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; A6: x in dom(g-h) by A3,A4,XBOOLE_0:def 4; thus (f1<->h).x = f1.x - h.x by A4,Th62 .= f.x + g.x - h.x by A5,Def41 .= f.x + (g.x - h.x) by Th13 .= f.x + ((g-h).x) by A6,VALUED_1:13 .= (f<+>(g-h)).x by A3,A4,Def41; end; theorem f <-> g <+> h = f <-> (g-h) proof set f1 = f<->g; A1: dom(g-h) = dom g /\ dom h by VALUED_1:12; A2: dom(f1<+>h) = dom f1 /\ dom h by Def41; dom f1 = dom f /\ dom g & dom(f<->(g-h)) = dom f /\ dom(g-h) by Th61; hence A3: dom(f1<+>h) = dom(f<->(g-h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1<+>h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; A6: x in dom(g-h) by A3,A4,XBOOLE_0:def 4; thus (f1<+>h).x = f1.x + h.x by A4,Def41 .= f.x - g.x + h.x by A5,Th62 .= f.x - (g.x - h.x) by Th14 .= f.x - ((g-h).x) by A6,VALUED_1:13 .= (f<->(g-h)).x by A3,A4,Th62; end; theorem f <-> g <-> h = f <-> (g+h) proof set f1 = f<->g; A1: dom(g+h) = dom g /\ dom h by VALUED_1:def 1; A2: dom(f1<->h) = dom f1 /\ dom h by Th61; dom f1 = dom f /\ dom g & dom(f<->(g+h)) = dom f /\ dom(g+h) by Th61; hence A3: dom(f1<->h) = dom(f<->(g+h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1<->h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; A6: x in dom(g+h) by A3,A4,XBOOLE_0:def 4; thus (f1<->h).x = f1.x - h.x by A4,Th62 .= f.x - g.x - h.x by A5,Th62 .= f.x - (g.x + h.x) by Th15 .= f.x - ((g+h).x) by A6,VALUED_1:def 1 .= (f<->(g+h)).x by A3,A4,Th62; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let g be complex-valued Function; deffunc F(object) = f.\$1(#)g.\$1; func f<#>g -> Function means :Def43: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x (#) g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let g be complex-valued Function; redefine func f<#>g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); coherence proof set h = f<#>g; A1: dom h = dom f /\ dom g by Def43; rng h c= C_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x (#) g.x by A2,Def43; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let g be real-valued Function; redefine func f<#>g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); coherence proof set h = f<#>g; A1: dom h = dom f /\ dom g by Def43; rng h c= R_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def43; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let g be RAT-valued Function; redefine func f<#>g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); coherence proof set h = f<#>g; A1: dom h = dom f /\ dom g by Def43; rng h c= Q_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def43; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be integer-functions-membered set; let f be PartFunc of X,Y; let g be INT-valued Function; redefine func f<#>g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); coherence proof set h = f<#>g; A1: dom h = dom f /\ dom g by Def43; rng h c= I_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def43; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X; let Y be natural-functions-membered set; let f be PartFunc of X,Y; let g be natural-valued Function; redefine func f<#>g -> PartFunc of X /\ dom g, N_PFuncs(DOMS(Y)); coherence proof set h = f<#>g; A1: dom h = dom f /\ dom g by Def43; rng h c= N_PFuncs(DOMS(Y)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def43; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y; then A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74; dom y = dom(f.x) by A3,A4,VALUED_1:def 5; then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem f <#> -g = (<->f) <#> g proof set f1 = <->f; A1: dom f1 = dom f & dom(f<#>-g) = dom f /\ dom -g by Def33,Def43; dom(f1<#>g) = dom f1 /\ dom g by Def43; hence A2: dom(f<#>-g) = dom(f1<#>g) by A1,VALUED_1:8; let x be object; assume A3: x in dom(f<#>-g); then A4: x in dom f1 by A1,XBOOLE_0:def 4; thus (f<#>-g).x = f.x (#) (-g).x by A3,Def43 .= f.x(#)-g.x by VALUED_1:8 .= (-f.x)(#)g.x by Th22 .= f1.x(#)g.x by A4,Def33 .= (f1<#>g).x by A2,A3,Def43; end; theorem f <#> -g = <-> (f <#> g) proof set f1 = f<#>g; A1: dom(<->f1) = dom f1 by Def33; dom f1 = dom f /\ dom g & dom(f<#>-g) = dom f /\ dom -g by Def43; hence A2: dom(f<#>-g) = dom(<->f1) by A1,VALUED_1:8; let x be object; assume A3: x in dom(f<#>-g); hence (f<#>-g).x = f.x (#) (-g).x by Def43 .= f.x(#)-g.x by VALUED_1:8 .= -(f.x(#)g.x) by Th24 .= -f1.x by A1,A2,A3,Def43 .= (<->f1).x by A2,A3,Def33; end; theorem f <#> g <#> h = f <#> (g(#)h) proof set f1 = f<#>g; A1: dom(g(#)h) = dom g /\ dom h by VALUED_1:def 4; A2: dom(f1<#>h) = dom f1 /\ dom h by Def43; dom f1 = dom f /\ dom g & dom(f<#>(g(#)h)) = dom f /\ dom(g(#)h) by Def43; hence A3: dom(f1<#>h) = dom(f<#>(g(#)h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1<#>h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; A6: x in dom(g(#)h) by A3,A4,XBOOLE_0:def 4; thus (f1<#>h).x = f1.x (#) h.x by A4,Def43 .= f.x (#) g.x (#) h.x by A5,Def43 .= f.x (#) (g.x * h.x) by Th16 .= f.x (#) ((g(#)h).x) by A6,VALUED_1:def 4 .= (f<#>(g(#)h)).x by A3,A4,Def43; end; definition let Y be complex-functions-membered set; let f be Y-valued Function; let g be complex-valued Function; func fg -> Function equals f <#> (g"); coherence; end; theorem Th71: dom(fg) = dom f /\ dom g proof thus dom(fg) = dom f /\ dom(g") by Def43 .= dom f /\ dom g by VALUED_1:def 7; end; theorem Th72: x in dom(fg) implies (fg).x = f.x (/) g.x proof assume x in dom(fg); hence (fg).x = f.x (#) (g").x by Def43 .= f.x (/) g.x by VALUED_1:10; end; definition let X; let Y be complex-functions-membered set; let f be PartFunc of X,Y; let g be complex-valued Function; redefine func fg -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); coherence proof fg = f <#> (g"); hence thesis by VALUED_1:def 7; end; end; definition let X; let Y be real-functions-membered set; let f be PartFunc of X,Y; let g be real-valued Function; redefine func fg -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); coherence proof fg = f <#> (g"); hence thesis by VALUED_1:def 7; end; end; definition let X; let Y be rational-functions-membered set; let f be PartFunc of X,Y; let g be RAT-valued Function; redefine func fg -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); coherence proof fg = f <#> (g"); hence thesis by VALUED_1:def 7; end; end; theorem f <#> g h = f <#> (g/"h) proof set f1 = f<#>g; A1: dom(g/"h) = dom g /\ dom h by VALUED_1:16; A2: dom(f1h) = dom f1 /\ dom h by Th71; dom f1 = dom f /\ dom g & dom(f<#>(g/"h)) = dom f /\ dom(g/"h) by Def43; hence A3: dom(f1h) = dom(f<#>(g/"h)) by A2,A1,XBOOLE_1:16; let x be object; assume A4: x in dom(f1h); then A5: x in dom f1 by A2,XBOOLE_0:def 4; thus (f1h).x = f1.x (/) h.x by A4,Th72 .= f.x (#) g.x (/) h.x by A5,Def43 .= f.x (#) (g.x / h.x) by Th16 .= f.x (#) ((g/"h).x) by VALUED_1:17 .= (f<#>(g/"h)).x by A3,A4,Def43; end; definition let Y1, Y2 be complex-functions-membered set; let f be Y1-valued Function; let g be Y2-valued Function; deffunc F(object) = f.\$1+g.\$1; func f<++>g -> Function means :Def45: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x + g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X1, X2 be set; let Y1, Y2 be complex-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<++>g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<++>g; A1: dom h = dom f /\ dom g by Def45; rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x + g.x by A2,Def45; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X1, X2 be set; let Y1, Y2 be real-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<++>g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<++>g; A1: dom h = dom f /\ dom g by Def45; rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def45; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be rational-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<++>g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<++>g; A1: dom h = dom f /\ dom g by Def45; rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def45; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be integer-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<++>g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<++>g; A1: dom h = dom f /\ dom g by Def45; rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def45; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be natural-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<++>g -> PartFunc of X1 /\ X2, N_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<++>g; A1: dom h = dom f /\ dom g by Def45; rng h c= N_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x + g.x by A2,Def45; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),NAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem f1 <++> f2 = f2 <++> f1 proof dom(f1<++>f2) = dom f1 /\ dom f2 by Def45; hence A1: dom(f1<++>f2) = dom(f2<++>f1) by Def45; let x be object; assume A2: x in dom(f1<++>f2); hence (f1<++>f2).x = f1.x + f2.x by Def45 .= (f2<++>f1).x by A1,A2,Def45; end; theorem f <++> f1 <++> f2 = f <++> (f1 <++> f2) proof set f3 = f<++>f1, f4 = f1<++>f2; A1: dom(f3<++>f2) = dom f3 /\ dom f2 by Def45; A2: dom(f<++>f4) = dom f /\ dom f4 by Def45; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45; hence A3: dom(f3<++>f2) = dom(f<++>f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<++>f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<++>f2).x = f3.x + f2.x by A4,Def45 .= f.x + f1.x + f2.x by A6,Def45 .= f.x + (f1.x + f2.x) by RFUNCT_1:8 .= f.x + f4.x by A5,Def45 .= (f<++>f4).x by A3,A4,Def45; end; theorem <-> (f1 <++> f2) = (<->f1) <++> (<->f2) proof set f3 = f1 <++> f2, f4 = <->f1, f5 = <->f2; A1: dom(f1 <++> f2) = dom f1 /\ dom f2 by Def45; A2: dom <->f2 = dom f2 by Def33; A3: dom <->f3 = dom f3 by Def33; A4: dom <->f1 = dom f1 by Def33; hence A5: dom(<->f3) = dom(f4<++>f5) by A1,A2,A3,Def45; let x be object; assume A6: x in dom(<->f3); then A7: x in dom f4 by A1,A4,A3,XBOOLE_0:def 4; A8: x in dom f5 by A1,A2,A3,A6,XBOOLE_0:def 4; thus (<->f3).x = -f3.x by A6,Def33 .= -(f1.x+f2.x) by A3,A6,Def45 .= -f1.x-f2.x by Th17 .= f4.x + -f2.x by A7,Def33 .= f4.x + f5.x by A8,Def33 .= (f4<++>f5).x by A5,A6,Def45; end; definition let Y1, Y2 be complex-functions-membered set; let f be Y1-valued Function; let g be Y2-valued Function; deffunc F(object) = f.\$1-g.\$1; func f<-->g -> Function means :Def46: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x - g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X1, X2 be set; let Y1, Y2 be complex-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<-->g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<-->g; A1: dom h = dom f /\ dom g by Def46; rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x - g.x by A2,Def46; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X1, X2 be set; let Y1, Y2 be real-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<-->g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<-->g; A1: dom h = dom f /\ dom g by Def46; rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Def46; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be rational-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<-->g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<-->g; A1: dom h = dom f /\ dom g by Def46; rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Def46; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be integer-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<-->g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<-->g; A1: dom h = dom f /\ dom g by Def46; rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x - g.x by A2,Def46; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; theorem f1 <--> f2 = <-> (f2 <--> f1) proof set f = f2<-->f1; A1: dom(f1<-->f2) = dom f1 /\ dom f2 & dom(f2<-->f1) = dom f2 /\ dom f1 by Def46; hence A2: dom(f1<-->f2) = dom<->f by Def33; let x be object; assume A3: x in dom(f1<-->f2); hence (f1<-->f2).x = f1.x-f2.x by Def46 .= -(f2.x-f1.x) by Th18 .= -f.x by A1,A3,Def46 .= (<->f).x by A2,A3,Def33; end; theorem <-> (f1 <--> f2) = (<->f1) <++> f2 proof set f3 = f1 <--> f2, f4 = <->f1; A1: dom <->f3 = dom f3 by Def33; A2: dom(f1 <--> f2) = dom f1 /\ dom f2 & dom <->f1 = dom f1 by Def33,Def46; hence A3: dom(<->f3) = dom(f4<++>f2) by A1,Def45; let x be object; assume A4: x in dom(<->f3); then A5: x in dom f4 by A2,A1,XBOOLE_0:def 4; thus (<->f3).x = -f3.x by A4,Def33 .= -(f1.x-f2.x) by A1,A4,Def46 .= -f1.x--f2.x by Th17 .= f4.x + f2.x by A5,Def33 .= (f4<++>f2).x by A3,A4,Def45; end; theorem f <++> f1 <--> f2 = f <++> (f1<-->f2) proof set f3 = f<++>f1, f4 = f1<-->f2; A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46; A2: dom(f<++>f4) = dom f /\ dom f4 by Def45; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45,Def46; hence A3: dom(f3<-->f2) = dom(f<++>f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<-->f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<-->f2).x = f3.x - f2.x by A4,Def46 .= f.x + f1.x - f2.x by A6,Def45 .= f.x + (f1.x - f2.x) by RFUNCT_1:8 .= f.x + f4.x by A5,Def46 .= (f<++>f4).x by A3,A4,Def45; end; theorem f <--> f1 <++> f2 = f <--> (f1 <--> f2) proof set f3 = f<-->f1, f4 = f1<-->f2; A1: dom(f3<++>f2) = dom f3 /\ dom f2 by Def45; A2: dom(f<-->f4) = dom f /\ dom f4 by Def46; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def46; hence A3: dom(f3<++>f2) = dom(f<-->f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<++>f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<++>f2).x = f3.x + f2.x by A4,Def45 .= f.x - f1.x + f2.x by A6,Def46 .= f.x - (f1.x - f2.x) by RFUNCT_1:22 .= f.x - f4.x by A5,Def46 .= (f<-->f4).x by A3,A4,Def46; end; theorem f <--> f1 <--> f2 = f <--> (f1 <++> f2) proof set f3 = f<-->f1, f4 = f1<++>f2; A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46; A2: dom(f<-->f4) = dom f /\ dom f4 by Def46; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45,Def46; hence A3: dom(f3<-->f2) = dom(f<-->f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<-->f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<-->f2).x = f3.x - f2.x by A4,Def46 .= f.x - f1.x - f2.x by A6,Def46 .= f.x - (f1.x + f2.x) by RFUNCT_1:20 .= f.x - f4.x by A5,Def45 .= (f<-->f4).x by A3,A4,Def46; end; theorem f <--> f1 <--> f2 = f <--> f2 <--> f1 proof set f3 = f<-->f1, f4 = f<-->f2; A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46; A2: dom(f4<-->f1) = dom f4 /\ dom f1 by Def46; dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def46; hence A3: dom(f3<-->f2) = dom(f4<-->f1) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<-->f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<-->f2).x = f3.x - f2.x by A4,Def46 .= f.x - f1.x - f2.x by A6,Def46 .= f.x - f2.x - f1.x by RFUNCT_1:23 .= f4.x - f1.x by A5,Def46 .= (f4<-->f1).x by A3,A4,Def46; end; definition let Y1, Y2 be complex-functions-membered set; let f be Y1-valued Function; let g be Y2-valued Function; deffunc F(object) = f.\$1(#)g.\$1; func f<##>g -> Function means :Def47: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x (#) g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X1, X2 be set; let Y1, Y2 be complex-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<##>g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<##>g; A1: dom h = dom f /\ dom g by Def47; rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x (#) g.x by A2,Def47; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X1, X2 be set; let Y1, Y2 be real-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<##>g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<##>g; A1: dom h = dom f /\ dom g by Def47; rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def47; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be rational-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<##>g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<##>g; A1: dom h = dom f /\ dom g by Def47; rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def47; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be integer-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<##>g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<##>g; A1: dom h = dom f /\ dom g by Def47; rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def47; A5: rng y c= INT by A3,A4,INT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def16; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be natural-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func f<##>g -> PartFunc of X1 /\ X2, N_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = f<##>g; A1: dom h = dom f /\ dom g by Def47; rng h c= N_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x (#) g.x by A2,Def47; A5: rng y c= NAT by A3,A4,ORDINAL1:def 12; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),NAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def18; end; hence thesis by A1,RELSET_1:4; end; end; theorem Th83: f1 <##> f2 = f2 <##> f1 proof dom(f1<##>f2) = dom f1 /\ dom f2 by Def47; hence A1: dom(f1<##>f2) = dom(f2<##>f1) by Def47; let x be object; assume A2: x in dom(f1<##>f2); hence (f1<##>f2).x = f1.x (#) f2.x by Def47 .= (f2<##>f1).x by A1,A2,Def47; end; theorem (f <##> f1) <##> f2 = f <##> (f1 <##> f2) proof set f3 = f<##>f1, f4 = f1<##>f2; A1: dom(f3<##>f2) = dom f3 /\ dom f2 by Def47; A2: dom(f<##>f4) = dom f /\ dom f4 by Def47; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47; hence A3: dom(f3<##>f2) = dom(f<##>f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<##>f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<##>f2).x = f3.x (#) f2.x by A4,Def47 .= f.x (#) f1.x (#) f2.x by A6,Def47 .= f.x (#) (f1.x (#) f2.x) by RFUNCT_1:9 .= f.x (#) f4.x by A5,Def47 .= (f<##>f4).x by A3,A4,Def47; end; theorem (<->f1) <##> f2 = <-> (f1<##>f2) proof set f3 = f1<##>f2, f4 = <->f1; A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f1 by Def33,Def47; dom(f4<##>f2) = dom f4 /\ dom f2 by Def47; hence A2: dom(f4<##>f2) = dom(<->f3) by A1,Def33; let x be object; assume A3: x in dom(f4<##>f2); then A4: x in dom f3 by A1,Def47; then A5: x in dom <->f1 by A1,XBOOLE_0:def 4; thus (f4<##>f2).x = f4.x (#) f2.x by A3,Def47 .= (-(f1.x)) (#) f2.x by A5,Def33 .= -(f1.x) (#) f2.x by Th25 .= -f3.x by A4,Def47 .= (<->f3).x by A2,A3,Def33; end; theorem f1 <##> <->f2 = <-> (f1<##>f2) proof set f3 = f1<##>f2, f4 = <->f2; A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f2 by Def33,Def47; dom(f1<##>f4) = dom f1 /\ dom f4 by Def47; hence A2: dom(f1<##>f4) = dom(<->f3) by A1,Def33; let x be object; assume A3: x in dom(f1<##>f4); then A4: x in dom f3 by A1,Def47; then A5: x in dom <->f2 by A1,XBOOLE_0:def 4; thus (f1<##>f4).x = f1.x (#) f4.x by A3,Def47 .= f1.x (#) -f2.x by A5,Def33 .= -(f1.x) (#) f2.x by Th25 .= -f3.x by A4,Def47 .= (<->f3).x by A2,A3,Def33; end; theorem Th87: f <##> (f1<++>f2) = (f<##>f1) <++> (f<##>f2) proof set f3 = f<##>f1, f4 = f<##>f2, f5 = f1<++>f2; A1: dom(f<##>f5) = dom f /\ dom f5 by Def47; A2: dom f5 = dom f1 /\ dom f2 by Def45; A3: dom(f3<++>f4) = dom f3 /\ dom f4 by Def45; dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47; hence A4: dom(f<##>f5) = dom(f3<++>f4) by A1,A3,A2,Lm1; let x be object; assume A5: x in dom(f<##>f5); then A6: x in dom f3 by A3,A4,XBOOLE_0:def 4; A7: x in dom f5 by A1,A5,XBOOLE_0:def 4; A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4; thus (f<##>f5).x = f.x (#) f5.x by A5,Def47 .= f.x (#) (f1.x + f2.x) by A7,Def45 .= f.x (#) f1.x + f.x (#) f2.x by RFUNCT_1:10 .= f3.x + f.x (#) f2.x by A6,Def47 .= f3.x + f4.x by A8,Def47 .= (f3<++>f4).x by A4,A5,Def45; end; theorem (f1<++>f2) <##> f = (f1<##>f) <++> (f2<##>f) proof set f3 = f1<##>f, f4 = f2<##>f, f5 = f1<++>f2; A1: f1<##>f = f<##>f1 & f2<##>f = f<##>f2 by Th83; thus f5 <##> f = f <##> f5 by Th83 .= f3 <++> f4 by A1,Th87; end; theorem Th89: f <##> (f1<-->f2) = (f<##>f1) <--> (f<##>f2) proof set f3 = f<##>f1, f4 = f<##>f2, f5 = f1<-->f2; A1: dom(f<##>f5) = dom f /\ dom f5 by Def47; A2: dom f5 = dom f1 /\ dom f2 by Def46; A3: dom(f3<-->f4) = dom f3 /\ dom f4 by Def46; dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47; hence A4: dom(f<##>f5) = dom(f3<-->f4) by A1,A3,A2,Lm1; let x be object; assume A5: x in dom(f<##>f5); then A6: x in dom f3 by A3,A4,XBOOLE_0:def 4; A7: x in dom f5 by A1,A5,XBOOLE_0:def 4; A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4; thus (f<##>f5).x = f.x (#) f5.x by A5,Def47 .= f.x (#) (f1.x - f2.x) by A7,Def46 .= f.x (#) f1.x - f.x (#) f2.x by RFUNCT_1:15 .= f3.x - f.x (#) f2.x by A6,Def47 .= f3.x - f4.x by A8,Def47 .= (f3<-->f4).x by A4,A5,Def46; end; theorem (f1<-->f2) <##> f = (f1<##>f) <--> (f2<##>f) proof set f3 = f1<##>f, f4 = f2<##>f, f5 = f1<-->f2; A1: f1<##>f = f<##>f1 & f2<##>f = f<##>f2 by Th83; thus f5 <##> f = f <##> f5 by Th83 .= f3 <--> f4 by A1,Th89; end; definition let Y1, Y2 be complex-functions-membered set; let f be Y1-valued Function; let g be Y2-valued Function; deffunc F(object) = f.\$1/"g.\$1; func fg -> Function means :Def48: dom it = dom f /\ dom g & for x being object st x in dom it holds it.x = f.x /" g.x; existence proof ex F being Function st dom F = dom f /\ dom g & for x being object st x in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let F,G be Function such that A1: dom F = dom f /\ dom g and A2: for x being object st x in dom F holds F.x = F(x) and A3: dom G = dom f /\ dom g and A4: for x being object st x in dom G holds G.x = F(x); thus dom F = dom G by A1,A3; let x be object; assume A5: x in dom F; hence F.x = F(x) by A2 .= G.x by A1,A3,A4,A5; end; end; definition let X1, X2 be set; let Y1, Y2 be complex-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func fg -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = fg; A1: dom h = dom f /\ dom g by Def48; rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; A4: h.x = f.x /" g.x by A2,Def48; then reconsider y as Function by A3; A5: rng y c= COMPLEX by A3,A4,XCMPLX_0:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def8; end; hence thesis by A1,RELSET_1:4,XBOOLE_1:27; end; end; definition let X1, X2 be set; let Y1, Y2 be real-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func fg -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = fg; A1: dom h = dom f /\ dom g by Def48; rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x /" g.x by A2,Def48; A5: rng y c= REAL by A3,A4,XREAL_0:def 1; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def12; end; hence thesis by A1,RELSET_1:4; end; end; definition let X1, X2 be set; let Y1, Y2 be rational-functions-membered set; let f be PartFunc of X1,Y1; let g be PartFunc of X2,Y2; redefine func fg -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); coherence proof set h = fg; A1: dom h = dom f /\ dom g by Def48; rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2)) proof let y be object; assume y in rng h; then consider x being object such that A2: x in dom h and A3: h.x = y by FUNCT_1:def 3; reconsider y as Function by A3; A4: h.x = f.x /" g.x by A2,Def48; A5: rng y c= RAT by A3,A4,RAT_1:def 2; x in dom g by A1,A2,XBOOLE_0:def 4; then g.x in Y2 by PARTFUN1:4; then dom(g.x) in the set of all dom m where m is Element of Y2; then A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74; x in dom f by A1,A2,XBOOLE_0:def 4; then f.x in Y1 by PARTFUN1:4; then dom(f.x) in the set of all dom m where m is Element of Y1; then A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74; dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16; then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4 ,XBOOLE_1:27; hence thesis by Def14; end; hence thesis by A1,RELSET_1:4; end; end; theorem (<->f1) f2 = <-> (f1f2) proof set f3 = f1f2, f4 = <->f1; A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f1 by Def33,Def48; dom(f4f2) = dom f4 /\ dom f2 by Def48; hence A2: dom(f4f2) = dom(<->f3) by A1,Def33; let x be object; assume A3: x in dom(f4f2); then A4: x in dom f3 by A1,Def48; then A5: x in dom <->f1 by A1,XBOOLE_0:def 4; thus (f4f2).x = f4.x /" f2.x by A3,Def48 .= (-(f1.x)) /" f2.x by A5,Def33 .= -(f1.x) /" f2.x by Th25 .= -f3.x by A4,Def48 .= (<->f3).x by A2,A3,Def33; end; theorem f1 <->f2 = <-> (f1f2) proof set f3 = f1f2, f4 = <->f2; A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f2 by Def33,Def48; dom(f1f4) = dom f1 /\ dom f4 by Def48; hence A2: dom(f1f4) = dom(<->f3) by A1,Def33; let x be object; assume A3: x in dom(f1f4); then A4: x in dom f3 by A1,Def48; then A5: x in dom <->f2 by A1,XBOOLE_0:def 4; thus (f1f4).x = f1.x /" f4.x by A3,Def48 .= f1.x /" -f2.x by A5,Def33 .= -(f1.x) /" f2.x by Th27 .= -f3.x by A4,Def48 .= (<->f3).x by A2,A3,Def33; end; theorem f <##> f1 f2 = f <##> (f1f2) proof set f3 = f<##>f1, f4 = f1f2; A1: dom(f3f2) = dom f3 /\ dom f2 by Def48; A2: dom(f<##>f4) = dom f /\ dom f4 by Def47; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47,Def48; hence A3: dom(f3f2) = dom(f<##>f4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3f2).x = f3.x /" f2.x by A4,Def48 .= f.x (#) f1.x /" f2.x by A6,Def47 .= f.x (#) (f1.x /" f2.x) by Th19 .= f.x (#) f4.x by A5,Def48 .= (f<##>f4).x by A3,A4,Def47; end; theorem f f1 <##> f2 = f <##> f2 f1 proof set f3 = ff1, f4 = f<##>f2; A1: dom(f3<##>f2) = dom f3 /\ dom f2 by Def47; A2: dom(f4f1) = dom f4 /\ dom f1 by Def48; dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47,Def48; hence A3: dom(f3<##>f2) = dom(f4f1) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3<##>f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3<##>f2).x = f3.x (#) f2.x by A4,Def47 .= f.x /" f1.x (#) f2.x by A6,Def48 .= f.x (#) f2.x /" f1.x by Th20 .= f4.x /" f1.x by A5,Def47 .= (f4f1).x by A3,A4,Def48; end; theorem f f1 f2 = f (f1 <##> f2) proof set f3 = ff1, f4 = f1<##>f2; A1: dom(f3f2) = dom f3 /\ dom f2 by Def48; A2: dom(ff4) = dom f /\ dom f4 by Def48; dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47,Def48; hence A3: dom(f3f2) = dom(ff4) by A1,A2,XBOOLE_1:16; let x be object; assume A4: x in dom(f3f2); then A5: x in dom f4 by A2,A3,XBOOLE_0:def 4; A6: x in dom f3 by A1,A4,XBOOLE_0:def 4; thus (f3f2).x = f3.x /" f2.x by A4,Def48 .= f.x /" f1.x /" f2.x by A6,Def48 .= f.x /" (f1.x (#) f2.x) by Th21 .= f.x /" f4.x by A5,Def47 .= (ff4).x by A3,A4,Def48; end; theorem (f1<++>f2) f = (f1f) <++> (f2f) proof set f3 = f1f, f4 = f2f, f5 = f1<++>f2; A1: dom(f5f) = dom f /\ dom f5 by Def48; A2: dom f5 = dom f1 /\ dom f2 by Def45; A3: dom(f3<++>f4) = dom f3 /\ dom f4 by Def45; dom f3 = dom f1 /\ dom f & dom f4 = dom f2 /\ dom f by Def48; hence A4: dom(f5f) = dom(f3<++>f4) by A1,A3,A2,Lm1; let x be object; assume A5: x in dom(f5f); then A6: x in dom f3 by A3,A4,XBOOLE_0:def 4; A7: x in dom f5 by A1,A5,XBOOLE_0:def 4; A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4; thus (f5f).x = f5.x /" f.x by A5,Def48 .= (f1.x+f2.x) /" f.x by A7,Def45 .= f1.x /" f.x + f2.x /" f.x by RFUNCT_1:10 .= f3.x + f2.x /" f.x by A6,Def48 .= f3.x + f4.x by A8,Def48 .= (f3<++>f4).x by A4,A5,Def45; end; theorem (f1<-->f2) f = (f1f) <--> (f2f) proof set f3 = f1f, f4 = f2f, f5 = f1<-->f2; A1: dom(f5f) = dom f /\ dom f5 by Def48; A2: dom f5 = dom f1 /\ dom f2 by Def46; A3: dom(f3<-->f4) = dom f3 /\ dom f4 by Def46; dom f3 = dom f1 /\ dom f & dom f4 = dom f2 /\ dom f by Def48; hence A4: dom(f5f) = dom(f3<-->f4) by A1,A3,A2,Lm1; let x be object; assume A5: x in dom(f5f); then A6: x in dom f3 by A3,A4,XBOOLE_0:def 4; A7: x in dom f5 by A1,A5,XBOOLE_0:def 4; A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4; thus (f5f).x = f5.x /" f.x by A5,Def48 .= (f1.x-f2.x) /" f.x by A7,Def46 .= f1.x /" f.x - f2.x /" f.x by RFUNCT_1:14 .= f3.x - f2.x /" f.x by A6,Def48 .= f3.x - f4.x by A8,Def48 .= (f3<-->f4).x by A4,A5,Def46; end;