:: Arithmetic Operations on Functions from Sets into Functional Sets :: by Artur Korni{\l}owicz :: :: Received October 15, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin Lm1: now__::_thesis:_for_X1,_X2,_X3_being_set_holds_X1_/\_(X2_/\_X3)_=_(X1_/\_X2)_/\_(X1_/\_X3) let X1, X2, X3 be set ; ::_thesis: X1 /\ (X2 /\ X3) = (X1 /\ X2) /\ (X1 /\ X3) 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 ; ::_thesis: verum end; definition let Y be functional set ; func DOMS Y -> set equals :: VALUED_2:def 1 union { (dom f) where f is Element of Y : verum } ; coherence union { (dom f) where f is Element of Y : verum } is set ; end; :: deftheorem defines DOMS VALUED_2:def_1_:_ for Y being functional set holds DOMS Y = union { (dom f) where f is Element of Y : verum } ; definition let X be set ; attrX is complex-functions-membered means :Def2: :: VALUED_2:def 2 for x being set st x in X holds x is complex-valued Function; end; :: deftheorem Def2 defines complex-functions-membered VALUED_2:def_2_:_ for X being set holds ( X is complex-functions-membered iff for x being set st x in X holds x is complex-valued Function ); definition let X be set ; attrX is ext-real-functions-membered means :Def3: :: VALUED_2:def 3 for x being set st x in X holds x is ext-real-valued Function; end; :: deftheorem Def3 defines ext-real-functions-membered VALUED_2:def_3_:_ for X being set holds ( X is ext-real-functions-membered iff for x being set st x in X holds x is ext-real-valued Function ); definition let X be set ; attrX is real-functions-membered means :Def4: :: VALUED_2:def 4 for x being set st x in X holds x is real-valued Function; end; :: deftheorem Def4 defines real-functions-membered VALUED_2:def_4_:_ for X being set holds ( X is real-functions-membered iff for x being set st x in X holds x is real-valued Function ); definition let X be set ; attrX is rational-functions-membered means :Def5: :: VALUED_2:def 5 for x being set st x in X holds x is RAT -valued Function; end; :: deftheorem Def5 defines rational-functions-membered VALUED_2:def_5_:_ for X being set holds ( X is rational-functions-membered iff for x being set st x in X holds x is RAT -valued Function ); definition let X be set ; attrX is integer-functions-membered means :Def6: :: VALUED_2:def 6 for x being set st x in X holds x is INT -valued Function; end; :: deftheorem Def6 defines integer-functions-membered VALUED_2:def_6_:_ for X being set holds ( X is integer-functions-membered iff for x being set st x in X holds x is INT -valued Function ); definition let X be set ; attrX is natural-functions-membered means :Def7: :: VALUED_2:def 7 for x being set st x in X holds x is natural-valued Function; end; :: deftheorem Def7 defines natural-functions-membered VALUED_2:def_7_:_ for X being set holds ( X is natural-functions-membered iff for x being set st x in X holds x is natural-valued Function ); registration cluster natural-functions-membered -> integer-functions-membered for set ; coherence for b1 being set st b1 is natural-functions-membered holds b1 is integer-functions-membered proofend; cluster integer-functions-membered -> rational-functions-membered for set ; coherence for b1 being set st b1 is integer-functions-membered holds b1 is rational-functions-membered proofend; cluster rational-functions-membered -> real-functions-membered for set ; coherence for b1 being set st b1 is rational-functions-membered holds b1 is real-functions-membered proofend; cluster real-functions-membered -> complex-functions-membered for set ; coherence for b1 being set st b1 is real-functions-membered holds b1 is complex-functions-membered proofend; cluster real-functions-membered -> ext-real-functions-membered for set ; coherence for b1 being set st b1 is real-functions-membered holds b1 is ext-real-functions-membered proofend; end; registration cluster empty -> natural-functions-membered for set ; coherence for b1 being set st b1 is empty holds b1 is natural-functions-membered proofend; end; registration let f be complex-valued Function; cluster{f} -> complex-functions-membered ; coherence {f} is complex-functions-membered proofend; end; registration cluster complex-functions-membered -> functional for set ; coherence for b1 being set st b1 is complex-functions-membered holds b1 is functional proofend; cluster ext-real-functions-membered -> functional for set ; coherence for b1 being set st b1 is ext-real-functions-membered holds b1 is functional proofend; end; set ff = the natural-valued Function; registration cluster non empty natural-functions-membered for set ; existence ex b1 being set st ( b1 is natural-functions-membered & not b1 is empty ) proofend; end; registration let X be complex-functions-membered set ; cluster -> complex-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is complex-functions-membered proofend; end; registration let X be ext-real-functions-membered set ; cluster -> ext-real-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is ext-real-functions-membered proofend; end; registration let X be real-functions-membered set ; cluster -> real-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is real-functions-membered proofend; end; registration let X be rational-functions-membered set ; cluster -> rational-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is rational-functions-membered proofend; end; registration let X be integer-functions-membered set ; cluster -> integer-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is integer-functions-membered proofend; end; registration let X be natural-functions-membered set ; cluster -> natural-functions-membered for Element of K19(X); coherence for b1 being Subset of X holds b1 is natural-functions-membered proofend; end; definition set A = COMPLEX ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,COMPLEX; func C_PFuncs D -> set means :Def8: :: VALUED_2:def 8 for f being set holds ( f in it iff f is PartFunc of D,COMPLEX ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,COMPLEX ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,COMPLEX ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,COMPLEX ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines C_PFuncs VALUED_2:def_8_:_ for D, b2 being set holds ( b2 = C_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,COMPLEX ) ); definition set A = COMPLEX ; let D be set ; defpred S1[ set ] means $1 is Function of D,COMPLEX; func C_Funcs D -> set means :Def9: :: VALUED_2:def 9 for f being set holds ( f in it iff f is Function of D,COMPLEX ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,COMPLEX ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,COMPLEX ) ) & ( for f being set holds ( f in b2 iff f is Function of D,COMPLEX ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines C_Funcs VALUED_2:def_9_:_ for D, b2 being set holds ( b2 = C_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,COMPLEX ) ); definition set A = ExtREAL ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,ExtREAL; func E_PFuncs D -> set means :Def10: :: VALUED_2:def 10 for f being set holds ( f in it iff f is PartFunc of D,ExtREAL ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,ExtREAL ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,ExtREAL ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,ExtREAL ) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines E_PFuncs VALUED_2:def_10_:_ for D, b2 being set holds ( b2 = E_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,ExtREAL ) ); definition set A = ExtREAL ; let D be set ; defpred S1[ set ] means $1 is Function of D,ExtREAL; func E_Funcs D -> set means :Def11: :: VALUED_2:def 11 for f being set holds ( f in it iff f is Function of D,ExtREAL ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,ExtREAL ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,ExtREAL ) ) & ( for f being set holds ( f in b2 iff f is Function of D,ExtREAL ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines E_Funcs VALUED_2:def_11_:_ for D, b2 being set holds ( b2 = E_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,ExtREAL ) ); definition set A = REAL ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,REAL; func R_PFuncs D -> set means :Def12: :: VALUED_2:def 12 for f being set holds ( f in it iff f is PartFunc of D,REAL ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,REAL ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,REAL ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,REAL ) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines R_PFuncs VALUED_2:def_12_:_ for D, b2 being set holds ( b2 = R_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,REAL ) ); definition set A = REAL ; let D be set ; defpred S1[ set ] means $1 is Function of D,REAL; func R_Funcs D -> set means :Def13: :: VALUED_2:def 13 for f being set holds ( f in it iff f is Function of D,REAL ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,REAL ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,REAL ) ) & ( for f being set holds ( f in b2 iff f is Function of D,REAL ) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines R_Funcs VALUED_2:def_13_:_ for D, b2 being set holds ( b2 = R_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,REAL ) ); definition set A = RAT ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,RAT; func Q_PFuncs D -> set means :Def14: :: VALUED_2:def 14 for f being set holds ( f in it iff f is PartFunc of D,RAT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,RAT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,RAT ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,RAT ) ) holds b1 = b2 proofend; end; :: deftheorem Def14 defines Q_PFuncs VALUED_2:def_14_:_ for D, b2 being set holds ( b2 = Q_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,RAT ) ); definition set A = RAT ; let D be set ; defpred S1[ set ] means $1 is Function of D,RAT; func Q_Funcs D -> set means :Def15: :: VALUED_2:def 15 for f being set holds ( f in it iff f is Function of D,RAT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,RAT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,RAT ) ) & ( for f being set holds ( f in b2 iff f is Function of D,RAT ) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines Q_Funcs VALUED_2:def_15_:_ for D, b2 being set holds ( b2 = Q_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,RAT ) ); definition set A = INT ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,INT; func I_PFuncs D -> set means :Def16: :: VALUED_2:def 16 for f being set holds ( f in it iff f is PartFunc of D,INT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,INT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,INT ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,INT ) ) holds b1 = b2 proofend; end; :: deftheorem Def16 defines I_PFuncs VALUED_2:def_16_:_ for D, b2 being set holds ( b2 = I_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,INT ) ); definition set A = INT ; let D be set ; defpred S1[ set ] means $1 is Function of D,INT; func I_Funcs D -> set means :Def17: :: VALUED_2:def 17 for f being set holds ( f in it iff f is Function of D,INT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,INT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,INT ) ) & ( for f being set holds ( f in b2 iff f is Function of D,INT ) ) holds b1 = b2 proofend; end; :: deftheorem Def17 defines I_Funcs VALUED_2:def_17_:_ for D, b2 being set holds ( b2 = I_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,INT ) ); definition set A = NAT ; let D be set ; defpred S1[ set ] means $1 is PartFunc of D,NAT; func N_PFuncs D -> set means :Def18: :: VALUED_2:def 18 for f being set holds ( f in it iff f is PartFunc of D,NAT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is PartFunc of D,NAT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is PartFunc of D,NAT ) ) & ( for f being set holds ( f in b2 iff f is PartFunc of D,NAT ) ) holds b1 = b2 proofend; end; :: deftheorem Def18 defines N_PFuncs VALUED_2:def_18_:_ for D, b2 being set holds ( b2 = N_PFuncs D iff for f being set holds ( f in b2 iff f is PartFunc of D,NAT ) ); definition set A = NAT ; let D be set ; defpred S1[ set ] means $1 is Function of D,NAT; func N_Funcs D -> set means :Def19: :: VALUED_2:def 19 for f being set holds ( f in it iff f is Function of D,NAT ); existence ex b1 being set st for f being set holds ( f in b1 iff f is Function of D,NAT ) proofend; uniqueness for b1, b2 being set st ( for f being set holds ( f in b1 iff f is Function of D,NAT ) ) & ( for f being set holds ( f in b2 iff f is Function of D,NAT ) ) holds b1 = b2 proofend; end; :: deftheorem Def19 defines N_Funcs VALUED_2:def_19_:_ for D, b2 being set holds ( b2 = N_Funcs D iff for f being set holds ( f in b2 iff f is Function of D,NAT ) ); theorem Th1: :: VALUED_2:1 for X being set holds C_Funcs X is Subset of (C_PFuncs X) proofend; theorem Th2: :: VALUED_2:2 for X being set holds E_Funcs X is Subset of (E_PFuncs X) proofend; theorem Th3: :: VALUED_2:3 for X being set holds R_Funcs X is Subset of (R_PFuncs X) proofend; theorem Th4: :: VALUED_2:4 for X being set holds Q_Funcs X is Subset of (Q_PFuncs X) proofend; theorem Th5: :: VALUED_2:5 for X being set holds I_Funcs X is Subset of (I_PFuncs X) proofend; theorem Th6: :: VALUED_2:6 for X being set holds N_Funcs X is Subset of (N_PFuncs X) proofend; registration let X be set ; cluster C_PFuncs X -> complex-functions-membered ; coherence C_PFuncs X is complex-functions-membered proofend; cluster C_Funcs X -> complex-functions-membered ; coherence C_Funcs X is complex-functions-membered proofend; cluster E_PFuncs X -> ext-real-functions-membered ; coherence E_PFuncs X is ext-real-functions-membered proofend; cluster E_Funcs X -> ext-real-functions-membered ; coherence E_Funcs X is ext-real-functions-membered proofend; cluster R_PFuncs X -> real-functions-membered ; coherence R_PFuncs X is real-functions-membered proofend; cluster R_Funcs X -> real-functions-membered ; coherence R_Funcs X is real-functions-membered proofend; cluster Q_PFuncs X -> rational-functions-membered ; coherence Q_PFuncs X is rational-functions-membered proofend; cluster Q_Funcs X -> rational-functions-membered ; coherence Q_Funcs X is rational-functions-membered proofend; cluster I_PFuncs X -> integer-functions-membered ; coherence I_PFuncs X is integer-functions-membered proofend; cluster I_Funcs X -> integer-functions-membered ; coherence I_Funcs X is integer-functions-membered proofend; cluster N_PFuncs X -> natural-functions-membered ; coherence N_PFuncs X is natural-functions-membered proofend; cluster N_Funcs X -> natural-functions-membered ; coherence N_Funcs X is natural-functions-membered proofend; end; registration let X be complex-functions-membered set ; cluster -> complex-valued for Element of X; coherence for b1 being Element of X holds b1 is complex-valued proofend; end; registration let X be ext-real-functions-membered set ; cluster -> ext-real-valued for Element of X; coherence for b1 being Element of X holds b1 is ext-real-valued proofend; end; registration let X be real-functions-membered set ; cluster -> real-valued for Element of X; coherence for b1 being Element of X holds b1 is real-valued proofend; end; registration let X be rational-functions-membered set ; cluster -> RAT -valued for Element of X; coherence for b1 being Element of X holds b1 is RAT -valued proofend; end; registration let X be integer-functions-membered set ; cluster -> INT -valued for Element of X; coherence for b1 being Element of X holds b1 is INT -valued proofend; end; registration let X be natural-functions-membered set ; cluster -> natural-valued for Element of X; coherence for b1 being Element of X holds b1 is natural-valued proofend; end; registration let X, x be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> Relation-like Function-like ; coherence ( f . x is Function-like & f . x is Relation-like ) ; end; registration let X, x be set ; let Y be ext-real-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> Relation-like Function-like ; coherence ( f . x is Function-like & f . x is Relation-like ) ; end; registration let X, x be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> complex-valued ; coherence f . x is complex-valued proofend; end; registration let X, x be set ; let Y be ext-real-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> ext-real-valued ; coherence f . x is ext-real-valued proofend; end; registration let X, x be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> real-valued ; coherence f . x is real-valued proofend; end; registration let X, x be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> RAT -valued ; coherence f . x is RAT -valued proofend; end; registration let X, x be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> INT -valued ; coherence f . x is INT -valued proofend; end; registration let X, x be set ; let Y be natural-functions-membered set ; let f be PartFunc of X,Y; clusterf . x -> natural-valued ; coherence f . x is natural-valued proofend; end; registration let X be set ; let Y be complex-membered set ; cluster PFuncs (X,Y) -> complex-functions-membered ; coherence PFuncs (X,Y) is complex-functions-membered proofend; end; registration let X be set ; let Y be ext-real-membered set ; cluster PFuncs (X,Y) -> ext-real-functions-membered ; coherence PFuncs (X,Y) is ext-real-functions-membered proofend; end; registration let X be set ; let Y be real-membered set ; cluster PFuncs (X,Y) -> real-functions-membered ; coherence PFuncs (X,Y) is real-functions-membered proofend; end; registration let X be set ; let Y be rational-membered set ; cluster PFuncs (X,Y) -> rational-functions-membered ; coherence PFuncs (X,Y) is rational-functions-membered proofend; end; registration let X be set ; let Y be integer-membered set ; cluster PFuncs (X,Y) -> integer-functions-membered ; coherence PFuncs (X,Y) is integer-functions-membered proofend; end; registration let X be set ; let Y be natural-membered set ; cluster PFuncs (X,Y) -> natural-functions-membered ; coherence PFuncs (X,Y) is natural-functions-membered proofend; end; registration let X be set ; let Y be complex-membered set ; cluster Funcs (X,Y) -> complex-functions-membered ; coherence Funcs (X,Y) is complex-functions-membered proofend; end; registration let X be set ; let Y be ext-real-membered set ; cluster Funcs (X,Y) -> ext-real-functions-membered ; coherence Funcs (X,Y) is ext-real-functions-membered proofend; end; registration let X be set ; let Y be real-membered set ; cluster Funcs (X,Y) -> real-functions-membered ; coherence Funcs (X,Y) is real-functions-membered proofend; end; registration let X be set ; let Y be rational-membered set ; cluster Funcs (X,Y) -> rational-functions-membered ; coherence Funcs (X,Y) is rational-functions-membered proofend; end; registration let X be set ; let Y be integer-membered set ; cluster Funcs (X,Y) -> integer-functions-membered ; coherence Funcs (X,Y) is integer-functions-membered proofend; end; registration let X be set ; let Y be natural-membered set ; cluster Funcs (X,Y) -> natural-functions-membered ; coherence Funcs (X,Y) is natural-functions-membered proofend; end; definition let R be Relation; attrR is complex-functions-valued means :Def20: :: VALUED_2:def 20 rng R is complex-functions-membered ; attrR is ext-real-functions-valued means :Def21: :: VALUED_2:def 21 rng R is ext-real-functions-membered ; attrR is real-functions-valued means :Def22: :: VALUED_2:def 22 rng R is real-functions-membered ; attrR is rational-functions-valued means :Def23: :: VALUED_2:def 23 rng R is rational-functions-membered ; attrR is integer-functions-valued means :Def24: :: VALUED_2:def 24 rng R is integer-functions-membered ; attrR is natural-functions-valued means :Def25: :: VALUED_2:def 25 rng R is natural-functions-membered ; end; :: deftheorem Def20 defines complex-functions-valued VALUED_2:def_20_:_ for R being Relation holds ( R is complex-functions-valued iff rng R is complex-functions-membered ); :: deftheorem Def21 defines ext-real-functions-valued VALUED_2:def_21_:_ for R being Relation holds ( R is ext-real-functions-valued iff rng R is ext-real-functions-membered ); :: deftheorem Def22 defines real-functions-valued VALUED_2:def_22_:_ for R being Relation holds ( R is real-functions-valued iff rng R is real-functions-membered ); :: deftheorem Def23 defines rational-functions-valued VALUED_2:def_23_:_ for R being Relation holds ( R is rational-functions-valued iff rng R is rational-functions-membered ); :: deftheorem Def24 defines integer-functions-valued VALUED_2:def_24_:_ for R being Relation holds ( R is integer-functions-valued iff rng R is integer-functions-membered ); :: deftheorem Def25 defines natural-functions-valued VALUED_2:def_25_:_ for R being Relation holds ( R is natural-functions-valued iff rng R is natural-functions-membered ); registration let Y be complex-functions-membered set ; cluster Relation-like Y -valued Function-like -> Y -valued complex-functions-valued for set ; coherence for b1 being Y -valued Function holds b1 is complex-functions-valued proofend; end; definition let f be Function; redefine attr f is complex-functions-valued means :: VALUED_2:def 26 for x being set st x in dom f holds f . x is complex-valued Function; compatibility ( f is complex-functions-valued iff for x being set st x in dom f holds f . x is complex-valued Function ) proofend; redefine attr f is ext-real-functions-valued means :: VALUED_2:def 27 for x being set st x in dom f holds f . x is ext-real-valued Function; compatibility ( f is ext-real-functions-valued iff for x being set st x in dom f holds f . x is ext-real-valued Function ) proofend; redefine attr f is real-functions-valued means :: VALUED_2:def 28 for x being set st x in dom f holds f . x is real-valued Function; compatibility ( f is real-functions-valued iff for x being set st x in dom f holds f . x is real-valued Function ) proofend; redefine attr f is rational-functions-valued means :: VALUED_2:def 29 for x being set st x in dom f holds f . x is RAT -valued Function; compatibility ( f is rational-functions-valued iff for x being set st x in dom f holds f . x is RAT -valued Function ) proofend; redefine attr f is integer-functions-valued means :: VALUED_2:def 30 for x being set st x in dom f holds f . x is INT -valued Function; compatibility ( f is integer-functions-valued iff for x being set st x in dom f holds f . x is INT -valued Function ) proofend; redefine attr f is natural-functions-valued means :: VALUED_2:def 31 for x being set st x in dom f holds f . x is natural-valued Function; compatibility ( f is natural-functions-valued iff for x being set st x in dom f holds f . x is natural-valued Function ) proofend; end; :: deftheorem defines complex-functions-valued VALUED_2:def_26_:_ for f being Function holds ( f is complex-functions-valued iff for x being set st x in dom f holds f . x is complex-valued Function ); :: deftheorem defines ext-real-functions-valued VALUED_2:def_27_:_ for f being Function holds ( f is ext-real-functions-valued iff for x being set st x in dom f holds f . x is ext-real-valued Function ); :: deftheorem defines real-functions-valued VALUED_2:def_28_:_ for f being Function holds ( f is real-functions-valued iff for x being set st x in dom f holds f . x is real-valued Function ); :: deftheorem defines rational-functions-valued VALUED_2:def_29_:_ for f being Function holds ( f is rational-functions-valued iff for x being set st x in dom f holds f . x is RAT -valued Function ); :: deftheorem defines integer-functions-valued VALUED_2:def_30_:_ for f being Function holds ( f is integer-functions-valued iff for x being set st x in dom f holds f . x is INT -valued Function ); :: deftheorem defines natural-functions-valued VALUED_2:def_31_:_ for f being Function holds ( f is natural-functions-valued iff for x being set st x in dom f holds f . x is natural-valued Function ); registration cluster Relation-like natural-functions-valued -> integer-functions-valued for set ; coherence for b1 being Relation st b1 is natural-functions-valued holds b1 is integer-functions-valued proofend; cluster Relation-like integer-functions-valued -> rational-functions-valued for set ; coherence for b1 being Relation st b1 is integer-functions-valued holds b1 is rational-functions-valued proofend; cluster Relation-like rational-functions-valued -> real-functions-valued for set ; coherence for b1 being Relation st b1 is rational-functions-valued holds b1 is real-functions-valued proofend; cluster Relation-like real-functions-valued -> ext-real-functions-valued for set ; coherence for b1 being Relation st b1 is real-functions-valued holds b1 is ext-real-functions-valued proofend; cluster Relation-like real-functions-valued -> complex-functions-valued for set ; coherence for b1 being Relation st b1 is real-functions-valued holds b1 is complex-functions-valued proofend; end; registration cluster Relation-like empty -> natural-functions-valued for set ; coherence for b1 being Relation st b1 is empty holds b1 is natural-functions-valued proofend; end; registration cluster Relation-like Function-like natural-functions-valued for set ; existence ex b1 being Function st b1 is natural-functions-valued proofend; end; registration let R be complex-functions-valued Relation; cluster rng R -> complex-functions-membered ; coherence rng R is complex-functions-membered by Def20; end; registration let R be ext-real-functions-valued Relation; cluster rng R -> ext-real-functions-membered ; coherence rng R is ext-real-functions-membered by Def21; end; registration let R be real-functions-valued Relation; cluster rng R -> real-functions-membered ; coherence rng R is real-functions-membered by Def22; end; registration let R be rational-functions-valued Relation; cluster rng R -> rational-functions-membered ; coherence rng R is rational-functions-membered by Def23; end; registration let R be integer-functions-valued Relation; cluster rng R -> integer-functions-membered ; coherence rng R is integer-functions-membered by Def24; end; registration let R be natural-functions-valued Relation; cluster rng R -> natural-functions-membered ; coherence rng R is natural-functions-membered by Def25; end; registration let X be set ; let Y be complex-functions-membered set ; cluster Function-like -> complex-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is complex-functions-valued ; end; registration let X be set ; let Y be ext-real-functions-membered set ; cluster Function-like -> ext-real-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is ext-real-functions-valued proofend; end; registration let X be set ; let Y be real-functions-membered set ; cluster Function-like -> real-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is real-functions-valued proofend; end; registration let X be set ; let Y be rational-functions-membered set ; cluster Function-like -> rational-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is rational-functions-valued proofend; end; registration let X be set ; let Y be integer-functions-membered set ; cluster Function-like -> integer-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is integer-functions-valued proofend; end; registration let X be set ; let Y be natural-functions-membered set ; cluster Function-like -> natural-functions-valued for Element of K19(K20(X,Y)); coherence for b1 being PartFunc of X,Y holds b1 is natural-functions-valued proofend; end; registration let f be complex-functions-valued Function; let x be set ; clusterf . x -> Relation-like Function-like ; coherence ( f . x is Function-like & f . x is Relation-like ) proofend; end; registration let f be ext-real-functions-valued Function; let x be set ; clusterf . x -> Relation-like Function-like ; coherence ( f . x is Function-like & f . x is Relation-like ) proofend; end; registration let f be complex-functions-valued Function; let x be set ; clusterf . x -> complex-valued ; coherence f . x is complex-valued proofend; end; registration let f be ext-real-functions-valued Function; let x be set ; clusterf . x -> ext-real-valued ; coherence f . x is ext-real-valued proofend; end; registration let f be real-functions-valued Function; let x be set ; clusterf . x -> real-valued ; coherence f . x is real-valued proofend; end; registration let f be rational-functions-valued Function; let x be set ; clusterf . x -> RAT -valued ; coherence f . x is RAT -valued proofend; end; registration let f be integer-functions-valued Function; let x be set ; clusterf . x -> INT -valued ; coherence f . x is INT -valued proofend; end; registration let f be natural-functions-valued Function; let x be set ; clusterf . x -> natural-valued ; coherence f . x is natural-valued proofend; end; begin theorem Th7: :: VALUED_2:7 for c1, c2 being complex number for g being complex-valued Function st g <> {} & g + c1 = g + c2 holds c1 = c2 proofend; theorem Th8: :: VALUED_2:8 for c1, c2 being complex number for g being complex-valued Function st g <> {} & g - c1 = g - c2 holds c1 = c2 proofend; theorem Th9: :: VALUED_2:9 for c1, c2 being complex number for g being complex-valued Function st g <> {} & g is non-empty & g (#) c1 = g (#) c2 holds c1 = c2 proofend; theorem Th10: :: VALUED_2:10 for c being complex number for g being complex-valued Function holds - (g + c) = (- g) - c proofend; theorem Th11: :: VALUED_2:11 for c being complex number for g being complex-valued Function holds - (g - c) = (- g) + c proofend; theorem Th12: :: VALUED_2:12 for c1, c2 being complex number for g being complex-valued Function holds (g + c1) + c2 = g + (c1 + c2) proofend; theorem Th13: :: VALUED_2:13 for c1, c2 being complex number for g being complex-valued Function holds (g + c1) - c2 = g + (c1 - c2) proofend; theorem Th14: :: VALUED_2:14 for c1, c2 being complex number for g being complex-valued Function holds (g - c1) + c2 = g - (c1 - c2) proofend; theorem Th15: :: VALUED_2:15 for c1, c2 being complex number for g being complex-valued Function holds (g - c1) - c2 = g - (c1 + c2) proofend; theorem Th16: :: VALUED_2:16 for c1, c2 being complex number for g being complex-valued Function holds (g (#) c1) (#) c2 = g (#) (c1 * c2) proofend; theorem Th17: :: VALUED_2:17 for g, h being complex-valued Function holds - (g + h) = (- g) - h proofend; theorem Th18: :: VALUED_2:18 for g, h being complex-valued Function holds g - h = - (h - g) proofend; theorem Th19: :: VALUED_2:19 for g, h, k being complex-valued Function holds (g (#) h) /" k = g (#) (h /" k) proofend; theorem Th20: :: VALUED_2:20 for g, h, k being complex-valued Function holds (g /" h) (#) k = (g (#) k) /" h proofend; theorem Th21: :: VALUED_2:21 for g, h, k being complex-valued Function holds (g /" h) /" k = g /" (h (#) k) proofend; theorem Th22: :: VALUED_2:22 for c being complex number for g being complex-valued Function holds c (#) (- g) = (- c) (#) g proofend; theorem Th23: :: VALUED_2:23 for c being complex number for g being complex-valued Function holds c (#) (- g) = - (c (#) g) proofend; theorem Th24: :: VALUED_2:24 for c being complex number for g being complex-valued Function holds (- c) (#) g = - (c (#) g) proofend; theorem Th25: :: VALUED_2:25 for g, h being complex-valued Function holds - (g (#) h) = (- g) (#) h proofend; theorem :: VALUED_2:26 for g, h being complex-valued Function holds - (g /" h) = (- g) /" h proofend; theorem Th27: :: VALUED_2:27 for g, h being complex-valued Function holds - (g /" h) = g /" (- h) proofend; definition let f be complex-valued Function; let c be complex number ; funcf (/) c -> Function equals :: VALUED_2:def 32 (1 / c) (#) f; coherence (1 / c) (#) f is Function ; end; :: deftheorem defines (/) VALUED_2:def_32_:_ for f being complex-valued Function for c being complex number holds f (/) c = (1 / c) (#) f; registration let f be complex-valued Function; let c be complex number ; clusterf (/) c -> complex-valued ; coherence f (/) c is complex-valued ; end; registration let f be real-valued Function; let r be real number ; clusterf (/) r -> real-valued ; coherence f (/) r is real-valued ; end; registration let f be RAT -valued Function; let r be rational number ; clusterf (/) r -> RAT -valued ; coherence f (/) r is RAT -valued ; end; registration let f be complex-valued FinSequence; let c be complex number ; clusterf (/) c -> FinSequence-like ; coherence f (/) c is FinSequence-like ; end; theorem :: VALUED_2:28 for c being complex number for g being complex-valued Function holds dom (g (/) c) = dom g by VALUED_1:def_5; theorem :: VALUED_2:29 for x being set for c being complex number for g being complex-valued Function holds (g (/) c) . x = (g . x) / c by VALUED_1:6; theorem Th30: :: VALUED_2:30 for c being complex number for g being complex-valued Function holds (- g) (/) c = - (g (/) c) proofend; theorem Th31: :: VALUED_2:31 for c being complex number for g being complex-valued Function holds g (/) (- c) = - (g (/) c) proofend; theorem :: VALUED_2:32 for c being complex number for g being complex-valued Function holds g (/) (- c) = (- g) (/) c proofend; theorem Th33: :: VALUED_2:33 for c1, c2 being complex number for g being complex-valued Function st g <> {} & g is non-empty & g (/) c1 = g (/) c2 holds c1 = c2 proofend; theorem :: VALUED_2:34 for c1, c2 being complex number for g being complex-valued Function holds (g (#) c1) (/) c2 = g (#) (c1 / c2) proofend; theorem :: VALUED_2:35 for c1, c2 being complex number for g being complex-valued Function holds (g (/) c1) (#) c2 = (g (#) c2) (/) c1 proofend; theorem :: VALUED_2:36 for c1, c2 being complex number for g being complex-valued Function holds (g (/) c1) (/) c2 = g (/) (c1 * c2) proofend; theorem :: VALUED_2:37 for c being complex number for g, h being complex-valued Function holds (g + h) (/) c = (g (/) c) + (h (/) c) proofend; theorem :: VALUED_2:38 for c being complex number for g, h being complex-valued Function holds (g - h) (/) c = (g (/) c) - (h (/) c) proofend; theorem :: VALUED_2:39 for c being complex number for g, h being complex-valued Function holds (g (#) h) (/) c = g (#) (h (/) c) proofend; theorem :: VALUED_2:40 for c being complex number for g, h being complex-valued Function holds (g /" h) (/) c = g /" (h (#) c) proofend; definition let f be complex-functions-valued Function; deffunc H1( set ) -> set = - (f . $1); func <-> f -> Function means :Def33: :: VALUED_2:def 33 ( dom it = dom f & ( for x being set st x in dom it holds it . x = - (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = - (f . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = - (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = - (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def33 defines <-> VALUED_2:def_33_:_ for f being complex-functions-valued Function for b2 being Function holds ( b2 = <-> f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = - (f . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; :: original:<-> redefine func <-> f -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence <-> f is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; :: original:<-> redefine func <-> f -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence <-> f is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; :: original:<-> redefine func <-> f -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence <-> f is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; :: original:<-> redefine func <-> f -> PartFunc of X,(I_PFuncs (DOMS Y)); coherence <-> f is PartFunc of X,(I_PFuncs (DOMS Y)) proofend; end; registration let Y be complex-functions-membered set ; let f be FinSequence of Y; cluster <-> f -> FinSequence-like ; coherence <-> f is FinSequence-like proofend; end; theorem :: VALUED_2:41 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y holds <-> (<-> f) = f proofend; theorem :: VALUED_2:42 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 st <-> f1 = <-> f2 holds f1 = f2 proofend; definition let X be complex-functions-membered set ; let Y be set ; let f be PartFunc of X,Y; defpred S1[ set , set ] means ex a being complex-valued Function st ( $1 = a & $2 = f . (- a) ); funcf (-) -> Function means :: VALUED_2:def 34 ( dom it = dom f & ( for x being complex-valued Function st x in dom it holds it . x = f . (- x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being complex-valued Function st x in dom b1 holds b1 . x = f . (- x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being complex-valued Function st x in dom b1 holds b1 . x = f . (- x) ) & dom b2 = dom f & ( for x being complex-valued Function st x in dom b2 holds b2 . x = f . (- x) ) holds b1 = b2 proofend; end; :: deftheorem defines (-) VALUED_2:def_34_:_ for X being complex-functions-membered set for Y being set for f being PartFunc of X,Y for b4 being Function holds ( b4 = f (-) iff ( dom b4 = dom f & ( for x being complex-valued Function st x in dom b4 holds b4 . x = f . (- x) ) ) ); definition let f be complex-functions-valued Function; deffunc H1( set ) -> set = (f . $1) " ; func f -> Function means :Def35: :: VALUED_2:def 35 ( dom it = dom f & ( for x being set st x in dom it holds it . x = (f . x) " ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = (f . x) " ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = (f . x) " ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = (f . x) " ) holds b1 = b2 proofend; end; :: deftheorem Def35 defines VALUED_2:def_35_:_ for f being complex-functions-valued Function for b2 being Function holds ( b2 = f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = (f . x) " ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; :: original: redefine func f -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence f is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; :: original: redefine func f -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence f is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; :: original: redefine func f -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence f is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; registration let Y be complex-functions-membered set ; let f be FinSequence of Y; cluster f -> FinSequence-like ; coherence f is FinSequence-like proofend; end; theorem :: VALUED_2:43 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y holds ( f) = f proofend; definition let f be complex-functions-valued Function; deffunc H1( set ) -> set = abs (f . $1); func abs f -> Function means :Def36: :: VALUED_2:def 36 ( dom it = dom f & ( for x being set st x in dom it holds it . x = abs (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = abs (f . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = abs (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = abs (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def36 defines abs VALUED_2:def_36_:_ for f being complex-functions-valued Function for b2 being Function holds ( b2 = abs f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = abs (f . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; :: original:abs redefine func abs f -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence abs f is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; :: original:abs redefine func abs f -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence abs f is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; :: original:abs redefine func abs f -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence abs f is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; :: original:abs redefine func abs f -> PartFunc of X,(N_PFuncs (DOMS Y)); coherence abs f is PartFunc of X,(N_PFuncs (DOMS Y)) proofend; end; registration let Y be complex-functions-membered set ; let f be FinSequence of Y; cluster abs f -> FinSequence-like ; coherence abs f is FinSequence-like proofend; end; theorem :: VALUED_2:44 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y holds abs (abs f) = abs f proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let c be complex number ; deffunc H1( set ) -> set = c + (f . $1); funcf [+] c -> Function means :Def37: :: VALUED_2:def 37 ( dom it = dom f & ( for x being set st x in dom it holds it . x = c + (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = c + (f . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = c + (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = c + (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def37 defines [+] VALUED_2:def_37_:_ for Y being complex-functions-membered set for f being b1 -valued Function for c being complex number for b4 being Function holds ( b4 = f [+] c iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds b4 . x = c + (f . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let c be complex number ; :: original:[+] redefine funcf [+] c -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence f [+] c is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let c be real number ; :: original:[+] redefine funcf [+] c -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence f [+] c is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let c be rational number ; :: original:[+] redefine funcf [+] c -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence f [+] c is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let c be integer number ; :: original:[+] redefine funcf [+] c -> PartFunc of X,(I_PFuncs (DOMS Y)); coherence f [+] c is PartFunc of X,(I_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be natural-functions-membered set ; let f be PartFunc of X,Y; let c be Nat; :: original:[+] redefine funcf [+] c -> PartFunc of X,(N_PFuncs (DOMS Y)); coherence f [+] c is PartFunc of X,(N_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:45 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [+] c1) [+] c2 = f [+] (c1 + c2) proofend; theorem :: VALUED_2:46 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds c1 = c2 proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let c be complex number ; funcf [-] c -> Function equals :: VALUED_2:def 38 f [+] (- c); coherence f [+] (- c) is Function ; end; :: deftheorem defines [-] VALUED_2:def_38_:_ for Y being complex-functions-membered set for f being b1 -valued Function for c being complex number holds f [-] c = f [+] (- c); theorem :: VALUED_2:47 for X being set for Y being complex-functions-membered set for c being complex number for f being PartFunc of X,Y holds dom (f [-] c) = dom f by Def37; theorem :: VALUED_2:48 for X, x being set for Y being complex-functions-membered set for c being complex number for f being PartFunc of X,Y st x in dom (f [-] c) holds (f [-] c) . x = (f . x) - c by Def37; definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let c be complex number ; :: original:[-] redefine funcf [-] c -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence f [-] c is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let c be real number ; :: original:[-] redefine funcf [-] c -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence f [-] c is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let c be rational number ; :: original:[-] redefine funcf [-] c -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence f [-] c is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let c be integer number ; :: original:[-] redefine funcf [-] c -> PartFunc of X,(I_PFuncs (DOMS Y)); coherence f [-] c is PartFunc of X,(I_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:49 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y st f <> {} & f is non-empty & f [-] c1 = f [-] c2 holds c1 = c2 proofend; theorem :: VALUED_2:50 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [+] c1) [-] c2 = f [+] (c1 - c2) proofend; theorem :: VALUED_2:51 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [-] c1) [+] c2 = f [-] (c1 - c2) proofend; theorem :: VALUED_2:52 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [-] c1) [-] c2 = f [-] (c1 + c2) proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let c be complex number ; deffunc H1( set ) -> set = c (#) (f . $1); funcf [#] c -> Function means :Def39: :: VALUED_2:def 39 ( dom it = dom f & ( for x being set st x in dom it holds it . x = c (#) (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = c (#) (f . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = c (#) (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = c (#) (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def39 defines [#] VALUED_2:def_39_:_ for Y being complex-functions-membered set for f being b1 -valued Function for c being complex number for b4 being Function holds ( b4 = f [#] c iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds b4 . x = c (#) (f . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let c be complex number ; :: original:[#] redefine funcf [#] c -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence f [#] c is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let c be real number ; :: original:[#] redefine funcf [#] c -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence f [#] c is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let c be rational number ; :: original:[#] redefine funcf [#] c -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence f [#] c is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let c be integer number ; :: original:[#] redefine funcf [#] c -> PartFunc of X,(I_PFuncs (DOMS Y)); coherence f [#] c is PartFunc of X,(I_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be natural-functions-membered set ; let f be PartFunc of X,Y; let c be Nat; :: original:[#] redefine funcf [#] c -> PartFunc of X,(N_PFuncs (DOMS Y)); coherence f [#] c is PartFunc of X,(N_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:53 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [#] c1) [#] c2 = f [#] (c1 * c2) proofend; theorem :: VALUED_2:54 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y st f <> {} & f is non-empty & ( for x being set st x in dom f holds f . x is non-empty ) & f [#] c1 = f [#] c2 holds c1 = c2 proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let c be complex number ; funcf [/] c -> Function equals :: VALUED_2:def 40 f [#] (c "); coherence f [#] (c ") is Function ; end; :: deftheorem defines [/] VALUED_2:def_40_:_ for Y being complex-functions-membered set for f being b1 -valued Function for c being complex number holds f [/] c = f [#] (c "); theorem :: VALUED_2:55 for X being set for Y being complex-functions-membered set for c being complex number for f being PartFunc of X,Y holds dom (f [/] c) = dom f by Def39; theorem :: VALUED_2:56 for X, x being set for Y being complex-functions-membered set for c being complex number for f being PartFunc of X,Y st x in dom (f [/] c) holds (f [/] c) . x = (c ") (#) (f . x) by Def39; definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let c be complex number ; :: original:[/] redefine funcf [/] c -> PartFunc of X,(C_PFuncs (DOMS Y)); coherence f [/] c is PartFunc of X,(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let c be real number ; :: original:[/] redefine funcf [/] c -> PartFunc of X,(R_PFuncs (DOMS Y)); coherence f [/] c is PartFunc of X,(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let c be rational number ; :: original:[/] redefine funcf [/] c -> PartFunc of X,(Q_PFuncs (DOMS Y)); coherence f [/] c is PartFunc of X,(Q_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:57 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2) proofend; theorem :: VALUED_2:58 for X being set for Y being complex-functions-membered set for c1, c2 being complex number for f being PartFunc of X,Y st f <> {} & f is non-empty & ( for x being set st x in dom f holds f . x is non-empty ) & f [/] c1 = f [/] c2 holds c1 = c2 proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let g be complex-valued Function; deffunc H1( set ) -> set = (f . $1) + (g . $1); funcf <+> g -> Function means :Def41: :: VALUED_2:def 41 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) + (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) + (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) + (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) + (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def41 defines <+> VALUED_2:def_41_:_ for Y being complex-functions-membered set for f being b1 -valued Function for g being complex-valued Function for b4 being Function holds ( b4 = f <+> g iff ( dom b4 = (dom f) /\ (dom g) & ( for x being set st x in dom b4 holds b4 . x = (f . x) + (g . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let g be complex-valued Function; :: original:<+> redefine funcf <+> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)); coherence f <+> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let g be real-valued Function; :: original:<+> redefine funcf <+> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)); coherence f <+> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let g be RAT -valued Function; :: original:<+> redefine funcf <+> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)); coherence f <+> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let g be INT -valued Function; :: original:<+> redefine funcf <+> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)); coherence f <+> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be natural-functions-membered set ; let f be PartFunc of X,Y; let g be natural-valued Function; :: original:<+> redefine funcf <+> g -> PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y)); coherence f <+> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:59 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <+> g) <+> h = f <+> (g + h) proofend; theorem :: VALUED_2:60 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds <-> (f <+> g) = (<-> f) <+> (- g) proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let g be complex-valued Function; funcf <-> g -> Function equals :: VALUED_2:def 42 f <+> (- g); coherence f <+> (- g) is Function ; end; :: deftheorem defines <-> VALUED_2:def_42_:_ for Y being complex-functions-membered set for f being b1 -valued Function for g being complex-valued Function holds f <-> g = f <+> (- g); theorem Th61: :: VALUED_2:61 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g) proofend; theorem Th62: :: VALUED_2:62 for X, x being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function st x in dom (f <-> g) holds (f <-> g) . x = (f . x) - (g . x) proofend; definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let g be complex-valued Function; :: original:<-> redefine funcf <-> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)); coherence f <-> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let g be real-valued Function; :: original:<-> redefine funcf <-> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)); coherence f <-> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let g be RAT -valued Function; :: original:<-> redefine funcf <-> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)); coherence f <-> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let g be INT -valued Function; :: original:<-> redefine funcf <-> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)); coherence f <-> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:63 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds f <-> (- g) = f <+> g ; theorem :: VALUED_2:64 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g proofend; theorem :: VALUED_2:65 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <+> g) <-> h = f <+> (g - h) proofend; theorem :: VALUED_2:66 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <-> g) <+> h = f <-> (g - h) proofend; theorem :: VALUED_2:67 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h) proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let g be complex-valued Function; deffunc H1( set ) -> set = (f . $1) (#) (g . $1); funcf <#> g -> Function means :Def43: :: VALUED_2:def 43 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) (#) (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) (#) (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) (#) (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) (#) (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def43 defines <#> VALUED_2:def_43_:_ for Y being complex-functions-membered set for f being b1 -valued Function for g being complex-valued Function for b4 being Function holds ( b4 = f <#> g iff ( dom b4 = (dom f) /\ (dom g) & ( for x being set st x in dom b4 holds b4 . x = (f . x) (#) (g . x) ) ) ); definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let g be complex-valued Function; :: original:<#> redefine funcf <#> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)); coherence f <#> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let g be real-valued Function; :: original:<#> redefine funcf <#> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)); coherence f <#> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let g be RAT -valued Function; :: original:<#> redefine funcf <#> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)); coherence f <#> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be integer-functions-membered set ; let f be PartFunc of X,Y; let g be INT -valued Function; :: original:<#> redefine funcf <#> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)); coherence f <#> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be natural-functions-membered set ; let f be PartFunc of X,Y; let g be natural-valued Function; :: original:<#> redefine funcf <#> g -> PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y)); coherence f <#> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:68 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds f <#> (- g) = (<-> f) <#> g proofend; theorem :: VALUED_2:69 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds f <#> (- g) = <-> (f <#> g) proofend; theorem :: VALUED_2:70 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <#> g) <#> h = f <#> (g (#) h) proofend; definition let Y be complex-functions-membered set ; let f be Y -valued Function; let g be complex-valued Function; funcf g -> Function equals :: VALUED_2:def 44 f <#> (g "); coherence f <#> (g ") is Function ; end; :: deftheorem defines VALUED_2:def_44_:_ for Y being complex-functions-membered set for f being b1 -valued Function for g being complex-valued Function holds f g = f <#> (g "); theorem Th71: :: VALUED_2:71 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function holds dom (f g) = (dom f) /\ (dom g) proofend; theorem Th72: :: VALUED_2:72 for X, x being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g being complex-valued Function st x in dom (f g) holds (f g) . x = (f . x) (/) (g . x) proofend; definition let X be set ; let Y be complex-functions-membered set ; let f be PartFunc of X,Y; let g be complex-valued Function; :: original: redefine funcf g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)); coherence f g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be real-functions-membered set ; let f be PartFunc of X,Y; let g be real-valued Function; :: original: redefine funcf g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)); coherence f g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y)) proofend; end; definition let X be set ; let Y be rational-functions-membered set ; let f be PartFunc of X,Y; let g be RAT -valued Function; :: original: redefine funcf g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)); coherence f g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)) proofend; end; theorem :: VALUED_2:73 for X being set for Y being complex-functions-membered set for f being PartFunc of X,Y for g, h being complex-valued Function holds (f <#> g) h = f <#> (g /" h) proofend; definition let Y1, Y2 be complex-functions-membered set ; let f be Y1 -valued Function; let g be Y2 -valued Function; deffunc H1( set ) -> set = (f . $1) + (g . $1); funcf <++> g -> Function means :Def45: :: VALUED_2:def 45 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) + (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) + (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) + (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) + (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def45 defines <++> VALUED_2:def_45_:_ for Y1, Y2 being complex-functions-membered set for f being b1 -valued Function for g being b2 -valued Function for b5 being Function holds ( b5 = f <++> g iff ( dom b5 = (dom f) /\ (dom g) & ( for x being set st x in dom b5 holds b5 . x = (f . x) + (g . x) ) ) ); 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; :: original:<++> redefine funcf <++> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <++> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<++> redefine funcf <++> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <++> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<++> redefine funcf <++> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <++> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<++> redefine funcf <++> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <++> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<++> redefine funcf <++> g -> PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <++> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; end; theorem :: VALUED_2:74 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f1 <++> f2 = f2 <++> f1 proofend; theorem :: VALUED_2:75 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <++> f1) <++> f2 = f <++> (f1 <++> f2) proofend; theorem :: VALUED_2:76 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds <-> (f1 <++> f2) = (<-> f1) <++> (<-> f2) proofend; definition let Y1, Y2 be complex-functions-membered set ; let f be Y1 -valued Function; let g be Y2 -valued Function; deffunc H1( set ) -> set = (f . $1) - (g . $1); funcf <--> g -> Function means :Def46: :: VALUED_2:def 46 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) - (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) - (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) - (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) - (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def46 defines <--> VALUED_2:def_46_:_ for Y1, Y2 being complex-functions-membered set for f being b1 -valued Function for g being b2 -valued Function for b5 being Function holds ( b5 = f <--> g iff ( dom b5 = (dom f) /\ (dom g) & ( for x being set st x in dom b5 holds b5 . x = (f . x) - (g . x) ) ) ); 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; :: original:<--> redefine funcf <--> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <--> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<--> redefine funcf <--> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <--> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<--> redefine funcf <--> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <--> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<--> redefine funcf <--> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <--> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; end; theorem :: VALUED_2:77 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f1 <--> f2 = <-> (f2 <--> f1) proofend; theorem :: VALUED_2:78 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds <-> (f1 <--> f2) = (<-> f1) <++> f2 proofend; theorem :: VALUED_2:79 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <++> f1) <--> f2 = f <++> (f1 <--> f2) proofend; theorem :: VALUED_2:80 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <--> f1) <++> f2 = f <--> (f1 <--> f2) proofend; theorem :: VALUED_2:81 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <--> f1) <--> f2 = f <--> (f1 <++> f2) proofend; theorem :: VALUED_2:82 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <--> f1) <--> f2 = (f <--> f2) <--> f1 proofend; definition let Y1, Y2 be complex-functions-membered set ; let f be Y1 -valued Function; let g be Y2 -valued Function; deffunc H1( set ) -> set = (f . $1) (#) (g . $1); funcf <##> g -> Function means :Def47: :: VALUED_2:def 47 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) (#) (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) (#) (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) (#) (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) (#) (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def47 defines <##> VALUED_2:def_47_:_ for Y1, Y2 being complex-functions-membered set for f being b1 -valued Function for g being b2 -valued Function for b5 being Function holds ( b5 = f <##> g iff ( dom b5 = (dom f) /\ (dom g) & ( for x being set st x in dom b5 holds b5 . x = (f . x) (#) (g . x) ) ) ); 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; :: original:<##> redefine funcf <##> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <##> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<##> redefine funcf <##> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <##> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<##> redefine funcf <##> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <##> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<##> redefine funcf <##> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <##> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original:<##> redefine funcf <##> g -> PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f <##> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; end; theorem Th83: :: VALUED_2:83 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f1 <##> f2 = f2 <##> f1 proofend; theorem :: VALUED_2:84 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <##> f1) <##> f2 = f <##> (f1 <##> f2) proofend; theorem :: VALUED_2:85 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (<-> f1) <##> f2 = <-> (f1 <##> f2) proofend; theorem :: VALUED_2:86 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f1 <##> (<-> f2) = <-> (f1 <##> f2) proofend; theorem Th87: :: VALUED_2:87 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f <##> (f1 <++> f2) = (f <##> f1) <++> (f <##> f2) proofend; theorem :: VALUED_2:88 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f1 <++> f2) <##> f = (f1 <##> f) <++> (f2 <##> f) proofend; theorem Th89: :: VALUED_2:89 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2) proofend; theorem :: VALUED_2:90 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) <##> f = (f1 <##> f) <--> (f2 <##> f) proofend; definition let Y1, Y2 be complex-functions-membered set ; let f be Y1 -valued Function; let g be Y2 -valued Function; deffunc H1( set ) -> set = (f . $1) /" (g . $1); funcf g -> Function means :Def48: :: VALUED_2:def 48 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = (f . x) /" (g . x) ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) /" (g . x) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = (f . x) /" (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = (f . x) /" (g . x) ) holds b1 = b2 proofend; end; :: deftheorem Def48 defines VALUED_2:def_48_:_ for Y1, Y2 being complex-functions-membered set for f being b1 -valued Function for g being b2 -valued Function for b5 being Function holds ( b5 = f g iff ( dom b5 = (dom f) /\ (dom g) & ( for x being set st x in dom b5 holds b5 . x = (f . x) /" (g . x) ) ) ); 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; :: original: redefine funcf g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original: redefine funcf g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; 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; :: original: redefine funcf g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))); coherence f g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2))) proofend; end; theorem :: VALUED_2:91 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (<-> f1) f2 = <-> (f1 f2) proofend; theorem :: VALUED_2:92 for X1, X2 being set for Y1, Y2 being complex-functions-membered set for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds f1 (<-> f2) = <-> (f1 f2) proofend; theorem :: VALUED_2:93 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f <##> f1) f2 = f <##> (f1 f2) proofend; theorem :: VALUED_2:94 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f f1) <##> f2 = (f <##> f2) f1 proofend; theorem :: VALUED_2:95 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f f1) f2 = f (f1 <##> f2) proofend; theorem :: VALUED_2:96 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f1 <++> f2) f = (f1 f) <++> (f2 f) proofend; theorem :: VALUED_2:97 for X, X1, X2 being set for Y, Y1, Y2 being complex-functions-membered set for f being PartFunc of X,Y for f1 being PartFunc of X1,Y1 for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) f = (f1 f) <--> (f2 f) proofend;