:: VALUED_0 semantic presentation begin definition let f be Relation; attrf is complex-valued means :Def1: :: VALUED_0:def 1 rng f c= COMPLEX ; attrf is ext-real-valued means :Def2: :: VALUED_0:def 2 rng f c= ExtREAL ; attrf is real-valued means :Def3: :: VALUED_0:def 3 rng f c= REAL ; canceled; canceled; attrf is natural-valued means :Def6: :: VALUED_0:def 6 rng f c= NAT ; end; :: deftheorem Def1 defines complex-valued VALUED_0:def_1_:_ for f being Relation holds ( f is complex-valued iff rng f c= COMPLEX ); :: deftheorem Def2 defines ext-real-valued VALUED_0:def_2_:_ for f being Relation holds ( f is ext-real-valued iff rng f c= ExtREAL ); :: deftheorem Def3 defines real-valued VALUED_0:def_3_:_ for f being Relation holds ( f is real-valued iff rng f c= REAL ); :: deftheorem VALUED_0:def_4_:_ canceled; :: deftheorem VALUED_0:def_5_:_ canceled; :: deftheorem Def6 defines natural-valued VALUED_0:def_6_:_ for f being Relation holds ( f is natural-valued iff rng f c= NAT ); registration cluster Relation-like natural-valued -> INT -valued for set ; coherence for b1 being Relation st b1 is natural-valued holds b1 is INT -valued proof let R be Relation; ::_thesis: ( R is natural-valued implies R is INT -valued ) assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is INT -valued hence rng R c= INT by NUMBERS:17, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; cluster Relation-like INT -valued -> RAT -valued for set ; coherence for b1 being Relation st b1 is INT -valued holds b1 is RAT -valued proof let R be Relation; ::_thesis: ( R is INT -valued implies R is RAT -valued ) assume rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is RAT -valued hence rng R c= RAT by NUMBERS:14, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; cluster Relation-like INT -valued -> real-valued for set ; coherence for b1 being Relation st b1 is INT -valued holds b1 is real-valued proof let R be Relation; ::_thesis: ( R is INT -valued implies R is real-valued ) assume rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued hence rng R c= REAL by XBOOLE_1:1, NUMBERS:15; :: according to VALUED_0:def_3 ::_thesis: verum end; cluster Relation-like RAT -valued -> real-valued for set ; coherence for b1 being Relation st b1 is RAT -valued holds b1 is real-valued proof let R be Relation; ::_thesis: ( R is RAT -valued implies R is real-valued ) assume rng R c= RAT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued hence rng R c= REAL by NUMBERS:12, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; cluster Relation-like real-valued -> ext-real-valued for set ; coherence for b1 being Relation st b1 is real-valued holds b1 is ext-real-valued proof let R be Relation; ::_thesis: ( R is real-valued implies R is ext-real-valued ) assume rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is ext-real-valued hence rng R c= ExtREAL by NUMBERS:31, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum end; cluster Relation-like real-valued -> complex-valued for set ; coherence for b1 being Relation st b1 is real-valued holds b1 is complex-valued proof let R be Relation; ::_thesis: ( R is real-valued implies R is complex-valued ) assume rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is complex-valued hence rng R c= COMPLEX by NUMBERS:11, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum end; cluster Relation-like natural-valued -> RAT -valued for set ; coherence for b1 being Relation st b1 is natural-valued holds b1 is RAT -valued proof let R be Relation; ::_thesis: ( R is natural-valued implies R is RAT -valued ) assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is RAT -valued hence rng R c= RAT by NUMBERS:18, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; cluster Relation-like natural-valued -> real-valued for set ; coherence for b1 being Relation st b1 is natural-valued holds b1 is real-valued proof let R be Relation; ::_thesis: ( R is natural-valued implies R is real-valued ) assume rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is real-valued hence rng R c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration cluster empty Relation-like -> natural-valued for set ; coherence for b1 being Relation st b1 is empty holds b1 is natural-valued proof let R be Relation; ::_thesis: ( R is empty implies R is natural-valued ) assume R is empty ; ::_thesis: R is natural-valued hence rng R c= NAT by RELAT_1:38, XBOOLE_1:2; :: according to VALUED_0:def_6 ::_thesis: verum end; end; registration cluster Relation-like Function-like natural-valued for set ; existence ex b1 being Function st b1 is natural-valued proof take {} ; ::_thesis: {} is natural-valued thus {} is natural-valued ; ::_thesis: verum end; end; registration let R be complex-valued Relation; cluster rng R -> complex-membered ; coherence rng R is complex-membered proof rng R c= COMPLEX by Def1; hence rng R is complex-membered ; ::_thesis: verum end; end; registration let R be ext-real-valued Relation; cluster rng R -> ext-real-membered ; coherence rng R is ext-real-membered proof rng R c= ExtREAL by Def2; hence rng R is ext-real-membered ; ::_thesis: verum end; end; registration let R be real-valued Relation; cluster rng R -> real-membered ; coherence rng R is real-membered proof rng R c= REAL by Def3; hence rng R is real-membered ; ::_thesis: verum end; end; registration let R be RAT -valued Relation; cluster rng R -> rational-membered ; coherence rng R is rational-membered ; end; registration let R be INT -valued Relation; cluster rng R -> integer-membered ; coherence rng R is integer-membered ; end; registration let R be natural-valued Relation; cluster rng R -> natural-membered ; coherence rng R is natural-membered proof rng R c= NAT by Def6; hence rng R is natural-membered ; ::_thesis: verum end; end; theorem Th1: :: VALUED_0:1 for R being Relation for S being complex-valued Relation st R c= S holds R is complex-valued proof let R be Relation; ::_thesis: for S being complex-valued Relation st R c= S holds R is complex-valued let S be complex-valued Relation; ::_thesis: ( R c= S implies R is complex-valued ) assume R c= S ; ::_thesis: R is complex-valued then A1: rng R c= rng S by RELAT_1:11; rng S c= COMPLEX by Def1; hence rng R c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum end; theorem Th2: :: VALUED_0:2 for R being Relation for S being ext-real-valued Relation st R c= S holds R is ext-real-valued proof let R be Relation; ::_thesis: for S being ext-real-valued Relation st R c= S holds R is ext-real-valued let S be ext-real-valued Relation; ::_thesis: ( R c= S implies R is ext-real-valued ) assume R c= S ; ::_thesis: R is ext-real-valued then A1: rng R c= rng S by RELAT_1:11; rng S c= ExtREAL by Def2; hence rng R c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum end; theorem Th3: :: VALUED_0:3 for R being Relation for S being real-valued Relation st R c= S holds R is real-valued proof let R be Relation; ::_thesis: for S being real-valued Relation st R c= S holds R is real-valued let S be real-valued Relation; ::_thesis: ( R c= S implies R is real-valued ) assume R c= S ; ::_thesis: R is real-valued then A1: rng R c= rng S by RELAT_1:11; rng S c= REAL by Def3; hence rng R c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; theorem :: VALUED_0:4 for R being Relation for S being RAT -valued Relation st R c= S holds R is RAT -valued ; theorem :: VALUED_0:5 for R being Relation for S being INT -valued Relation st R c= S holds R is INT -valued ; theorem Th6: :: VALUED_0:6 for R being Relation for S being natural-valued Relation st R c= S holds R is natural-valued proof let R be Relation; ::_thesis: for S being natural-valued Relation st R c= S holds R is natural-valued let S be natural-valued Relation; ::_thesis: ( R c= S implies R is natural-valued ) assume R c= S ; ::_thesis: R is natural-valued then A1: rng R c= rng S by RELAT_1:11; rng S c= NAT by Def6; hence rng R c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum end; registration let R be complex-valued Relation; cluster -> complex-valued for Element of bool R; coherence for b1 being Subset of R holds b1 is complex-valued by Th1; end; registration let R be ext-real-valued Relation; cluster -> ext-real-valued for Element of bool R; coherence for b1 being Subset of R holds b1 is ext-real-valued by Th2; end; registration let R be real-valued Relation; cluster -> real-valued for Element of bool R; coherence for b1 being Subset of R holds b1 is real-valued by Th3; end; registration let R be RAT -valued Relation; cluster -> RAT -valued for Element of bool R; coherence for b1 being Subset of R holds b1 is RAT -valued ; end; registration let R be INT -valued Relation; cluster -> INT -valued for Element of bool R; coherence for b1 being Subset of R holds b1 is INT -valued ; end; registration let R be natural-valued Relation; cluster -> natural-valued for Element of bool R; coherence for b1 being Subset of R holds b1 is natural-valued by Th6; end; registration let R, S be complex-valued Relation; clusterR \/ S -> complex-valued ; coherence R \/ S is complex-valued proof A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12; ( rng R c= COMPLEX & rng S c= COMPLEX ) by Def1; hence rng (R \/ S) c= COMPLEX by A1, XBOOLE_1:8; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let R, S be ext-real-valued Relation; clusterR \/ S -> ext-real-valued ; coherence R \/ S is ext-real-valued proof A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12; ( rng R c= ExtREAL & rng S c= ExtREAL ) by Def2; hence rng (R \/ S) c= ExtREAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let R, S be real-valued Relation; clusterR \/ S -> real-valued ; coherence R \/ S is real-valued proof A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12; ( rng R c= REAL & rng S c= REAL ) by Def3; hence rng (R \/ S) c= REAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let R, S be RAT -valued Relation; clusterR \/ S -> RAT -valued ; coherence R \/ S is RAT -valued ; end; registration let R, S be INT -valued Relation; clusterR \/ S -> INT -valued ; coherence R \/ S is INT -valued ; end; registration let R, S be natural-valued Relation; clusterR \/ S -> natural-valued ; coherence R \/ S is natural-valued proof A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12; ( rng R c= NAT & rng S c= NAT ) by Def6; hence rng (R \/ S) c= NAT by A1, XBOOLE_1:8; :: according to VALUED_0:def_6 ::_thesis: verum end; end; registration let R be complex-valued Relation; let S be Relation; clusterR /\ S -> complex-valued ; coherence R /\ S is complex-valued proof R /\ S c= R by XBOOLE_1:17; then A1: rng (R /\ S) c= rng R by RELAT_1:11; rng R c= COMPLEX by Def1; hence rng (R /\ S) c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum end; clusterR \ S -> complex-valued ; coherence R \ S is complex-valued ; end; registration let R be ext-real-valued Relation; let S be Relation; clusterR /\ S -> ext-real-valued ; coherence R /\ S is ext-real-valued proof R /\ S c= R by XBOOLE_1:17; then A1: rng (R /\ S) c= rng R by RELAT_1:11; rng R c= ExtREAL by Def2; hence rng (R /\ S) c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum end; clusterR \ S -> ext-real-valued ; coherence R \ S is ext-real-valued ; end; registration let R be real-valued Relation; let S be Relation; clusterR /\ S -> real-valued ; coherence R /\ S is real-valued proof R /\ S c= R by XBOOLE_1:17; then A1: rng (R /\ S) c= rng R by RELAT_1:11; rng R c= REAL by Def3; hence rng (R /\ S) c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; clusterR \ S -> real-valued ; coherence R \ S is real-valued ; end; registration let R be RAT -valued Relation; let S be Relation; clusterR /\ S -> RAT -valued ; coherence R /\ S is RAT -valued ; clusterR \ S -> RAT -valued ; coherence R \ S is RAT -valued ; end; registration let R be INT -valued Relation; let S be Relation; clusterR /\ S -> INT -valued ; coherence R /\ S is INT -valued ; clusterR \ S -> INT -valued ; coherence R \ S is INT -valued ; end; registration let R be natural-valued Relation; let S be Relation; clusterR /\ S -> natural-valued ; coherence R /\ S is natural-valued proof R /\ S c= R by XBOOLE_1:17; then A1: rng (R /\ S) c= rng R by RELAT_1:11; rng R c= NAT by Def6; hence rng (R /\ S) c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum end; clusterR \ S -> natural-valued ; coherence R \ S is natural-valued ; end; registration let R, S be complex-valued Relation; clusterR \+\ S -> complex-valued ; coherence R \+\ S is complex-valued ; end; registration let R, S be ext-real-valued Relation; clusterR \+\ S -> ext-real-valued ; coherence R \+\ S is ext-real-valued ; end; registration let R, S be real-valued Relation; clusterR \+\ S -> real-valued ; coherence R \+\ S is real-valued ; end; registration let R, S be RAT -valued Relation; clusterR \+\ S -> RAT -valued ; coherence R \+\ S is RAT -valued ; end; registration let R, S be INT -valued Relation; clusterR \+\ S -> INT -valued ; coherence R \+\ S is INT -valued ; end; registration let R, S be natural-valued Relation; clusterR \+\ S -> natural-valued ; coherence R \+\ S is natural-valued ; end; registration let R be complex-valued Relation; let X be set ; clusterR .: X -> complex-membered ; coherence R .: X is complex-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is complex-membered ; ::_thesis: verum end; end; registration let R be ext-real-valued Relation; let X be set ; clusterR .: X -> ext-real-membered ; coherence R .: X is ext-real-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is ext-real-membered ; ::_thesis: verum end; end; registration let R be real-valued Relation; let X be set ; clusterR .: X -> real-membered ; coherence R .: X is real-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is real-membered ; ::_thesis: verum end; end; registration let R be RAT -valued Relation; let X be set ; clusterR .: X -> rational-membered ; coherence R .: X is rational-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is rational-membered ; ::_thesis: verum end; end; registration let R be INT -valued Relation; let X be set ; clusterR .: X -> integer-membered ; coherence R .: X is integer-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is integer-membered ; ::_thesis: verum end; end; registration let R be natural-valued Relation; let X be set ; clusterR .: X -> natural-membered ; coherence R .: X is natural-membered proof R .: X c= rng R by RELAT_1:111; hence R .: X is natural-membered ; ::_thesis: verum end; end; registration let R be complex-valued Relation; let x be set ; cluster Im (R,x) -> complex-membered ; coherence Im (R,x) is complex-membered ; end; registration let R be ext-real-valued Relation; let x be set ; cluster Im (R,x) -> ext-real-membered ; coherence Im (R,x) is ext-real-membered ; end; registration let R be real-valued Relation; let x be set ; cluster Im (R,x) -> real-membered ; coherence Im (R,x) is real-membered ; end; registration let R be RAT -valued Relation; let x be set ; cluster Im (R,x) -> rational-membered ; coherence Im (R,x) is rational-membered ; end; registration let R be INT -valued Relation; let x be set ; cluster Im (R,x) -> integer-membered ; coherence Im (R,x) is integer-membered ; end; registration let R be natural-valued Relation; let x be set ; cluster Im (R,x) -> natural-membered ; coherence Im (R,x) is natural-membered ; end; registration let R be complex-valued Relation; let X be set ; clusterR | X -> complex-valued ; coherence R | X is complex-valued proof ( rng R c= COMPLEX & rng (R | X) c= rng R ) by Def1, RELAT_1:70; hence rng (R | X) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let R be ext-real-valued Relation; let X be set ; clusterR | X -> ext-real-valued ; coherence R | X is ext-real-valued proof ( rng R c= ExtREAL & rng (R | X) c= rng R ) by Def2, RELAT_1:70; hence rng (R | X) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let R be real-valued Relation; let X be set ; clusterR | X -> real-valued ; coherence R | X is real-valued proof ( rng R c= REAL & rng (R | X) c= rng R ) by Def3, RELAT_1:70; hence rng (R | X) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let R be RAT -valued Relation; let X be set ; clusterR | X -> RAT -valued ; coherence R | X is RAT -valued ; end; registration let R be INT -valued Relation; let X be set ; clusterR | X -> INT -valued ; coherence R | X is INT -valued ; end; registration let R be natural-valued Relation; let X be set ; clusterR | X -> natural-valued ; coherence R | X is natural-valued proof ( rng R c= NAT & rng (R | X) c= rng R ) by Def6, RELAT_1:70; hence rng (R | X) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum end; end; registration let X be complex-membered set ; cluster id X -> complex-valued ; coherence id X is complex-valued proof thus rng (id X) c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let X be ext-real-membered set ; cluster id X -> ext-real-valued ; coherence id X is ext-real-valued proof thus rng (id X) c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let X be real-membered set ; cluster id X -> real-valued ; coherence id X is real-valued proof thus rng (id X) c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let X be rational-membered set ; cluster id X -> RAT -valued ; coherence id X is RAT -valued proof thus rng (id X) c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be integer-membered set ; cluster id X -> INT -valued ; coherence id X is INT -valued proof thus rng (id X) c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be natural-membered set ; cluster id X -> natural-valued ; coherence id X is natural-valued proof thus rng (id X) c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum end; end; registration let R be Relation; let S be complex-valued Relation; clusterR * S -> complex-valued ; coherence R * S is complex-valued proof ( rng S c= COMPLEX & rng (R * S) c= rng S ) by Def1, RELAT_1:26; hence rng (R * S) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let R be Relation; let S be ext-real-valued Relation; clusterR * S -> ext-real-valued ; coherence R * S is ext-real-valued proof ( rng S c= ExtREAL & rng (R * S) c= rng S ) by Def2, RELAT_1:26; hence rng (R * S) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let R be Relation; let S be real-valued Relation; clusterR * S -> real-valued ; coherence R * S is real-valued proof ( rng S c= REAL & rng (R * S) c= rng S ) by Def3, RELAT_1:26; hence rng (R * S) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let R be Relation; let S be RAT -valued Relation; clusterR * S -> RAT -valued ; coherence R * S is RAT -valued ; end; registration let R be Relation; let S be INT -valued Relation; clusterR * S -> INT -valued ; coherence R * S is INT -valued ; end; registration let R be Relation; let S be natural-valued Relation; clusterR * S -> natural-valued ; coherence R * S is natural-valued proof ( rng S c= NAT & rng (R * S) c= rng S ) by Def6, RELAT_1:26; hence rng (R * S) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum end; end; definition let f be Function; redefine attr f is complex-valued means :Def7: :: VALUED_0:def 7 for x being set st x in dom f holds f . x is complex ; compatibility ( f is complex-valued iff for x being set st x in dom f holds f . x is complex ) proof thus ( f is complex-valued implies for x being set st x in dom f holds f . x is complex ) ::_thesis: ( ( for x being set st x in dom f holds f . x is complex ) implies f is complex-valued ) proof assume A1: f is complex-valued ; ::_thesis: for x being set st x in dom f holds f . x is complex let x be set ; ::_thesis: ( x in dom f implies f . x is complex ) assume A2: x in dom f ; ::_thesis: f . x is complex reconsider f = f as complex-valued Function by A1; f . x in rng f by A2, FUNCT_1:3; hence f . x is complex ; ::_thesis: verum end; assume A3: for x being set st x in dom f holds f . x is complex ; ::_thesis: f is complex-valued let y be set ; :: according to TARSKI:def_3,VALUED_0:def_1 ::_thesis: ( not y in rng f or y in COMPLEX ) assume y in rng f ; ::_thesis: y in COMPLEX then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; then y is complex by A3; hence y in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; redefine attr f is ext-real-valued means :Def8: :: VALUED_0:def 8 for x being set st x in dom f holds f . x is ext-real ; compatibility ( f is ext-real-valued iff for x being set st x in dom f holds f . x is ext-real ) proof thus ( f is ext-real-valued implies for x being set st x in dom f holds f . x is ext-real ) ::_thesis: ( ( for x being set st x in dom f holds f . x is ext-real ) implies f is ext-real-valued ) proof assume A4: f is ext-real-valued ; ::_thesis: for x being set st x in dom f holds f . x is ext-real let x be set ; ::_thesis: ( x in dom f implies f . x is ext-real ) assume A5: x in dom f ; ::_thesis: f . x is ext-real reconsider f = f as ext-real-valued Function by A4; f . x in rng f by A5, FUNCT_1:3; hence f . x is ext-real ; ::_thesis: verum end; assume A6: for x being set st x in dom f holds f . x is ext-real ; ::_thesis: f is ext-real-valued let y be set ; :: according to TARSKI:def_3,VALUED_0:def_2 ::_thesis: ( not y in rng f or y in ExtREAL ) assume y in rng f ; ::_thesis: y in ExtREAL then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; then y is ext-real by A6; hence y in ExtREAL by XXREAL_0:def_1; ::_thesis: verum end; redefine attr f is real-valued means :Def9: :: VALUED_0:def 9 for x being set st x in dom f holds f . x is real ; compatibility ( f is real-valued iff for x being set st x in dom f holds f . x is real ) proof thus ( f is real-valued implies for x being set st x in dom f holds f . x is real ) ::_thesis: ( ( for x being set st x in dom f holds f . x is real ) implies f is real-valued ) proof assume A7: f is real-valued ; ::_thesis: for x being set st x in dom f holds f . x is real let x be set ; ::_thesis: ( x in dom f implies f . x is real ) assume A8: x in dom f ; ::_thesis: f . x is real reconsider f = f as real-valued Function by A7; f . x in rng f by A8, FUNCT_1:3; hence f . x is real ; ::_thesis: verum end; assume A9: for x being set st x in dom f holds f . x is real ; ::_thesis: f is real-valued let y be set ; :: according to TARSKI:def_3,VALUED_0:def_3 ::_thesis: ( not y in rng f or y in REAL ) assume y in rng f ; ::_thesis: y in REAL then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; then y is real by A9; hence y in REAL by XREAL_0:def_1; ::_thesis: verum end; canceled; canceled; redefine attr f is natural-valued means :Def12: :: VALUED_0:def 12 for x being set st x in dom f holds f . x is natural ; compatibility ( f is natural-valued iff for x being set st x in dom f holds f . x is natural ) proof thus ( f is natural-valued implies for x being set st x in dom f holds f . x is natural ) ::_thesis: ( ( for x being set st x in dom f holds f . x is natural ) implies f is natural-valued ) proof assume A10: f is natural-valued ; ::_thesis: for x being set st x in dom f holds f . x is natural let x be set ; ::_thesis: ( x in dom f implies f . x is natural ) assume A11: x in dom f ; ::_thesis: f . x is natural reconsider f = f as natural-valued Function by A10; f . x in rng f by A11, FUNCT_1:3; hence f . x is natural ; ::_thesis: verum end; assume A12: for x being set st x in dom f holds f . x is natural ; ::_thesis: f is natural-valued let y be set ; :: according to TARSKI:def_3,VALUED_0:def_6 ::_thesis: ( not y in rng f or y in NAT ) assume y in rng f ; ::_thesis: y in NAT then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; then y is natural by A12; hence y in NAT by ORDINAL1:def_12; ::_thesis: verum end; end; :: deftheorem Def7 defines complex-valued VALUED_0:def_7_:_ for f being Function holds ( f is complex-valued iff for x being set st x in dom f holds f . x is complex ); :: deftheorem Def8 defines ext-real-valued VALUED_0:def_8_:_ for f being Function holds ( f is ext-real-valued iff for x being set st x in dom f holds f . x is ext-real ); :: deftheorem Def9 defines real-valued VALUED_0:def_9_:_ for f being Function holds ( f is real-valued iff for x being set st x in dom f holds f . x is real ); :: deftheorem VALUED_0:def_10_:_ canceled; :: deftheorem VALUED_0:def_11_:_ canceled; :: deftheorem Def12 defines natural-valued VALUED_0:def_12_:_ for f being Function holds ( f is natural-valued iff for x being set st x in dom f holds f . x is natural ); theorem Th7: :: VALUED_0:7 for f being Function holds ( f is complex-valued iff for x being set holds f . x is complex ) proof let f be Function; ::_thesis: ( f is complex-valued iff for x being set holds f . x is complex ) hereby ::_thesis: ( ( for x being set holds f . x is complex ) implies f is complex-valued ) assume A1: f is complex-valued ; ::_thesis: for x being set holds f . b2 is complex let x be set ; ::_thesis: f . b1 is complex percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is complex hence f . x is complex by A1, Def7; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is complex hence f . x is complex by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume for x being set holds f . x is complex ; ::_thesis: f is complex-valued then for x being set st x in dom f holds f . x is complex ; hence f is complex-valued by Def7; ::_thesis: verum end; theorem Th8: :: VALUED_0:8 for f being Function holds ( f is ext-real-valued iff for x being set holds f . x is ext-real ) proof let f be Function; ::_thesis: ( f is ext-real-valued iff for x being set holds f . x is ext-real ) hereby ::_thesis: ( ( for x being set holds f . x is ext-real ) implies f is ext-real-valued ) assume A1: f is ext-real-valued ; ::_thesis: for x being set holds f . b2 is ext-real let x be set ; ::_thesis: f . b1 is ext-real percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is ext-real hence f . x is ext-real by A1, Def8; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is ext-real hence f . x is ext-real by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume for x being set holds f . x is ext-real ; ::_thesis: f is ext-real-valued then for x being set st x in dom f holds f . x is ext-real ; hence f is ext-real-valued by Def8; ::_thesis: verum end; theorem Th9: :: VALUED_0:9 for f being Function holds ( f is real-valued iff for x being set holds f . x is real ) proof let f be Function; ::_thesis: ( f is real-valued iff for x being set holds f . x is real ) hereby ::_thesis: ( ( for x being set holds f . x is real ) implies f is real-valued ) assume A1: f is real-valued ; ::_thesis: for x being set holds f . b2 is real let x be set ; ::_thesis: f . b1 is real percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is real hence f . x is real by A1, Def9; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is real hence f . x is real by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume for x being set holds f . x is real ; ::_thesis: f is real-valued then for x being set st x in dom f holds f . x is real ; hence f is real-valued by Def9; ::_thesis: verum end; theorem Th10: :: VALUED_0:10 for f being Function holds ( f is RAT -valued iff for x being set holds f . x is rational ) proof let f be Function; ::_thesis: ( f is RAT -valued iff for x being set holds f . x is rational ) hereby ::_thesis: ( ( for x being set holds f . x is rational ) implies f is RAT -valued ) assume A1: f is RAT -valued ; ::_thesis: for x being set holds f . b2 is rational let x be set ; ::_thesis: f . b1 is rational percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is rational then f . x in rng f by FUNCT_1:def_3; hence f . x is rational by A1; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is rational hence f . x is rational by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume A2: for x being set holds f . x is rational ; ::_thesis: f is RAT -valued let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in RAT ) assume y in rng f ; ::_thesis: y in RAT then consider x being set such that x in dom f and A3: f . x = y by FUNCT_1:def_3; f . x is rational by A2; hence y in RAT by A3, RAT_1:def_2; ::_thesis: verum end; theorem Th11: :: VALUED_0:11 for f being Function holds ( f is INT -valued iff for x being set holds f . x is integer ) proof let f be Function; ::_thesis: ( f is INT -valued iff for x being set holds f . x is integer ) hereby ::_thesis: ( ( for x being set holds f . x is integer ) implies f is INT -valued ) assume A1: f is INT -valued ; ::_thesis: for x being set holds f . b2 is integer let x be set ; ::_thesis: f . b1 is integer percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is integer then f . x in rng f by FUNCT_1:def_3; hence f . x is integer by A1; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is integer hence f . x is integer by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume A2: for x being set holds f . x is integer ; ::_thesis: f is INT -valued let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in INT ) assume y in rng f ; ::_thesis: y in INT then consider x being set such that x in dom f and A3: f . x = y by FUNCT_1:def_3; f . x is integer by A2; hence y in INT by A3, INT_1:def_2; ::_thesis: verum end; theorem Th12: :: VALUED_0:12 for f being Function holds ( f is natural-valued iff for x being set holds f . x is natural ) proof let f be Function; ::_thesis: ( f is natural-valued iff for x being set holds f . x is natural ) hereby ::_thesis: ( ( for x being set holds f . x is natural ) implies f is natural-valued ) assume A1: f is natural-valued ; ::_thesis: for x being set holds f . b2 is natural let x be set ; ::_thesis: f . b1 is natural percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f . b1 is natural hence f . x is natural by A1, Def12; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . b1 is natural hence f . x is natural by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume for x being set holds f . x is natural ; ::_thesis: f is natural-valued then for x being set st x in dom f holds f . x is natural ; hence f is natural-valued by Def12; ::_thesis: verum end; registration let f be complex-valued Function; let x be set ; clusterf . x -> complex ; coherence f . x is complex by Th7; end; registration let f be ext-real-valued Function; let x be set ; clusterf . x -> ext-real ; coherence f . x is ext-real by Th8; end; registration let f be real-valued Function; let x be set ; clusterf . x -> real ; coherence f . x is real by Th9; end; registration let f be RAT -valued Function; let x be set ; clusterf . x -> rational ; coherence f . x is rational by Th10; end; registration let f be INT -valued Function; let x be set ; clusterf . x -> integer ; coherence f . x is integer by Th11; end; registration let f be natural-valued Function; let x be set ; clusterf . x -> natural ; coherence f . x is natural by Th12; end; registration let X be set ; let x be complex number ; clusterX --> x -> complex-valued ; coherence X --> x is complex-valued proof rng (X --> x) c= COMPLEX by MEMBERED:1; hence X --> x is complex-valued by Def1; ::_thesis: verum end; end; registration let X be set ; let x be ext-real number ; clusterX --> x -> ext-real-valued ; coherence X --> x is ext-real-valued proof rng (X --> x) c= ExtREAL by MEMBERED:2; hence X --> x is ext-real-valued by Def2; ::_thesis: verum end; end; registration let X be set ; let x be real number ; clusterX --> x -> real-valued ; coherence X --> x is real-valued proof rng (X --> x) c= REAL by MEMBERED:3; hence X --> x is real-valued by Def3; ::_thesis: verum end; end; registration let X be set ; let x be rational number ; clusterX --> x -> RAT -valued ; coherence X --> x is RAT -valued proof rng (X --> x) c= RAT by MEMBERED:4; hence X --> x is RAT -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let X be set ; let x be integer number ; clusterX --> x -> INT -valued ; coherence X --> x is INT -valued proof rng (X --> x) c= INT by MEMBERED:5; hence X --> x is INT -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let X be set ; let x be Nat; clusterX --> x -> natural-valued ; coherence X --> x is natural-valued proof rng (X --> x) c= NAT by MEMBERED:6; hence X --> x is natural-valued by Def6; ::_thesis: verum end; end; registration let f, g be complex-valued Function; clusterf +* g -> complex-valued ; coherence f +* g is complex-valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= COMPLEX by MEMBERED:1; hence f +* g is complex-valued by Def1; ::_thesis: verum end; end; registration let f, g be ext-real-valued Function; clusterf +* g -> ext-real-valued ; coherence f +* g is ext-real-valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= ExtREAL by MEMBERED:2; hence f +* g is ext-real-valued by Def2; ::_thesis: verum end; end; registration let f, g be real-valued Function; clusterf +* g -> real-valued ; coherence f +* g is real-valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= REAL by MEMBERED:3; hence f +* g is real-valued by Def3; ::_thesis: verum end; end; registration let f, g be RAT -valued Function; clusterf +* g -> RAT -valued ; coherence f +* g is RAT -valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= RAT by MEMBERED:4; hence f +* g is RAT -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let f, g be INT -valued Function; clusterf +* g -> INT -valued ; coherence f +* g is INT -valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= INT by MEMBERED:5; hence f +* g is INT -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let f, g be natural-valued Function; clusterf +* g -> natural-valued ; coherence f +* g is natural-valued proof rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then rng (f +* g) c= NAT by MEMBERED:6; hence f +* g is natural-valued by Def6; ::_thesis: verum end; end; registration let x be set ; let y be complex number ; clusterx .--> y -> complex-valued ; coherence x .--> y is complex-valued ; end; registration let x be set ; let y be ext-real number ; clusterx .--> y -> ext-real-valued ; coherence x .--> y is ext-real-valued ; end; registration let x be set ; let y be real number ; clusterx .--> y -> real-valued ; coherence x .--> y is real-valued ; end; registration let x be set ; let y be rational number ; clusterx .--> y -> RAT -valued ; coherence x .--> y is RAT -valued ; end; registration let x be set ; let y be integer number ; clusterx .--> y -> INT -valued ; coherence x .--> y is INT -valued ; end; registration let x be set ; let y be Nat; clusterx .--> y -> natural-valued ; coherence x .--> y is natural-valued ; end; registration let X be set ; let Y be complex-membered set ; cluster -> complex-valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is complex-valued proof let R be Relation of X,Y; ::_thesis: R is complex-valued thus rng R c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let X be set ; let Y be ext-real-membered set ; cluster -> ext-real-valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is ext-real-valued proof let R be Relation of X,Y; ::_thesis: R is ext-real-valued thus rng R c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let X be set ; let Y be real-membered set ; cluster -> real-valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is real-valued proof let R be Relation of X,Y; ::_thesis: R is real-valued thus rng R c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let X be set ; let Y be rational-membered set ; cluster -> RAT -valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is RAT -valued proof let R be Relation of X,Y; ::_thesis: R is RAT -valued thus rng R c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be set ; let Y be integer-membered set ; cluster -> INT -valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is INT -valued proof let R be Relation of X,Y; ::_thesis: R is INT -valued thus rng R c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be set ; let Y be natural-membered set ; cluster -> natural-valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is natural-valued proof let R be Relation of X,Y; ::_thesis: R is natural-valued thus rng R c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum end; end; registration let X be set ; let Y be complex-membered set ; cluster[:X,Y:] -> complex-valued ; coherence [:X,Y:] is complex-valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum end; end; registration let X be set ; let Y be ext-real-membered set ; cluster[:X,Y:] -> ext-real-valued ; coherence [:X,Y:] is ext-real-valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum end; end; registration let X be set ; let Y be real-membered set ; cluster[:X,Y:] -> real-valued ; coherence [:X,Y:] is real-valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum end; end; registration let X be set ; let Y be rational-membered set ; cluster[:X,Y:] -> RAT -valued ; coherence [:X,Y:] is RAT -valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be set ; let Y be integer-membered set ; cluster[:X,Y:] -> INT -valued ; coherence [:X,Y:] is INT -valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be set ; let Y be natural-membered set ; cluster[:X,Y:] -> natural-valued ; coherence [:X,Y:] is natural-valued proof rng [:X,Y:] c= Y by RELAT_1:159; hence rng [:X,Y:] c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum end; end; notation let f be ext-real-valued Relation; synonym non-zero f for non-empty ; end; registration cluster non empty Relation-like RAT -valued INT -valued Function-like constant natural-valued for set ; existence ex b1 being Function st ( not b1 is empty & b1 is constant & b1 is natural-valued & b1 is INT -valued & b1 is RAT -valued ) proof take 1 .--> 1 ; ::_thesis: ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued ) thus ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued ) ; ::_thesis: verum end; end; theorem :: VALUED_0:13 for f being non empty constant complex-valued Function ex r being complex number st for x being set st x in dom f holds f . x = r proof let f be non empty constant complex-valued Function; ::_thesis: ex r being complex number st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being complex number st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; theorem :: VALUED_0:14 for f being non empty constant ext-real-valued Function ex r being ext-real number st for x being set st x in dom f holds f . x = r proof let f be non empty constant ext-real-valued Function; ::_thesis: ex r being ext-real number st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being ext-real number st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; theorem :: VALUED_0:15 for f being non empty constant real-valued Function ex r being real number st for x being set st x in dom f holds f . x = r proof let f be non empty constant real-valued Function; ::_thesis: ex r being real number st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being real number st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; theorem :: VALUED_0:16 for f being non empty RAT -valued constant Function ex r being rational number st for x being set st x in dom f holds f . x = r proof let f be non empty RAT -valued constant Function; ::_thesis: ex r being rational number st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being rational number st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; theorem :: VALUED_0:17 for f being non empty INT -valued constant Function ex r being integer number st for x being set st x in dom f holds f . x = r proof let f be non empty INT -valued constant Function; ::_thesis: ex r being integer number st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being integer number st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; theorem :: VALUED_0:18 for f being non empty constant natural-valued Function ex r being Nat st for x being set st x in dom f holds f . x = r proof let f be non empty constant natural-valued Function; ::_thesis: ex r being Nat st for x being set st x in dom f holds f . x = r consider r being set such that A1: for x being set st x in dom f holds f . x = r by FUNCOP_1:78; consider x being set such that A2: x in dom f by XBOOLE_0:def_1; r = f . x by A1, A2; hence ex r being Nat st for x being set st x in dom f holds f . x = r by A1; ::_thesis: verum end; begin definition let f be ext-real-valued Function; attrf is increasing means :Def13: :: VALUED_0:def 13 for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 < f . e2; attrf is decreasing means :Def14: :: VALUED_0:def 14 for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 > f . e2; attrf is non-decreasing means :Def15: :: VALUED_0:def 15 for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 <= f . e2; attrf is non-increasing means :Def16: :: VALUED_0:def 16 for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 >= f . e2; end; :: deftheorem Def13 defines increasing VALUED_0:def_13_:_ for f being ext-real-valued Function holds ( f is increasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 < f . e2 ); :: deftheorem Def14 defines decreasing VALUED_0:def_14_:_ for f being ext-real-valued Function holds ( f is decreasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 > f . e2 ); :: deftheorem Def15 defines non-decreasing VALUED_0:def_15_:_ for f being ext-real-valued Function holds ( f is non-decreasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 <= f . e2 ); :: deftheorem Def16 defines non-increasing VALUED_0:def_16_:_ for f being ext-real-valued Function holds ( f is non-increasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 >= f . e2 ); registration cluster trivial Relation-like Function-like ext-real-valued -> ext-real-valued increasing decreasing for set ; coherence for b1 being ext-real-valued Function st b1 is trivial holds ( b1 is increasing & b1 is decreasing ) proof let f be ext-real-valued Function; ::_thesis: ( f is trivial implies ( f is increasing & f is decreasing ) ) assume A1: f is trivial ; ::_thesis: ( f is increasing & f is decreasing ) thus f is increasing ::_thesis: f is decreasing proof let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 < f . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 < f . e2 ) assume ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 < f . e2 ) hence ( not e1 < e2 or f . e1 < f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum end; let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds f . e1 > f . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 > f . e2 ) assume ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 > f . e2 ) hence ( not e1 < e2 or f . e1 > f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum end; end; registration cluster Relation-like Function-like ext-real-valued increasing -> ext-real-valued non-decreasing for set ; coherence for b1 being ext-real-valued Function st b1 is increasing holds b1 is non-decreasing proof let f be ext-real-valued Function; ::_thesis: ( f is increasing implies f is non-decreasing ) assume A1: f is increasing ; ::_thesis: f is non-decreasing let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 <= f . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 <= f . e2 ) assume that A2: ( e1 in dom f & e2 in dom f ) and A3: e1 <= e2 ; ::_thesis: f . e1 <= f . e2 percases ( e1 = e2 or e1 < e2 ) by A3, XXREAL_0:1; suppose e1 = e2 ; ::_thesis: f . e1 <= f . e2 hence f . e1 <= f . e2 ; ::_thesis: verum end; suppose e1 < e2 ; ::_thesis: f . e1 <= f . e2 hence f . e1 <= f . e2 by A1, A2, Def13; ::_thesis: verum end; end; end; cluster Relation-like Function-like ext-real-valued decreasing -> ext-real-valued non-increasing for set ; coherence for b1 being ext-real-valued Function st b1 is decreasing holds b1 is non-increasing proof let f be ext-real-valued Function; ::_thesis: ( f is decreasing implies f is non-increasing ) assume A4: f is decreasing ; ::_thesis: f is non-increasing let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds f . e1 >= f . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 >= f . e2 ) assume that A5: ( e1 in dom f & e2 in dom f ) and A6: e1 <= e2 ; ::_thesis: f . e1 >= f . e2 percases ( e1 = e2 or e1 < e2 ) by A6, XXREAL_0:1; suppose e1 = e2 ; ::_thesis: f . e1 >= f . e2 hence f . e1 >= f . e2 ; ::_thesis: verum end; suppose e1 < e2 ; ::_thesis: f . e1 >= f . e2 hence f . e1 >= f . e2 by A4, A5, Def14; ::_thesis: verum end; end; end; end; registration let f, g be ext-real-valued increasing Function; clusterf * g -> increasing ; coherence g * f is increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds (g * f) . e1 < (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2 then A7: f . e1 < f . e2 by A3, A5, Def13; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum end; end; registration let f, g be ext-real-valued non-decreasing Function; clusterf * g -> non-decreasing ; coherence g * f is non-decreasing proof let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds (g * f) . e1 <= (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2 then A7: f . e1 <= f . e2 by A3, A5, Def15; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum end; end; registration let f, g be ext-real-valued decreasing Function; clusterf * g -> increasing ; coherence g * f is increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds (g * f) . e1 < (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2 then A7: f . e1 > f . e2 by A3, A5, Def14; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def14; ::_thesis: verum end; end; registration let f, g be ext-real-valued non-increasing Function; clusterf * g -> non-decreasing ; coherence g * f is non-decreasing proof let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds (g * f) . e1 <= (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2 then A7: f . e1 >= f . e2 by A3, A5, Def16; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def16; ::_thesis: verum end; end; registration let f be ext-real-valued decreasing Function; let g be ext-real-valued increasing Function; clusterf * g -> decreasing ; coherence g * f is decreasing proof let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds (g * f) . e1 > (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 > (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 > (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 < e2 ; ::_thesis: (g * f) . e1 > (g * f) . e2 then A7: f . e1 > f . e2 by A3, A5, Def14; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 > (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum end; clusterg * f -> decreasing ; coherence f * g is decreasing proof let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 holds (f * g) . e1 > (f * g) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 implies (f * g) . e1 > (f * g) . e2 ) assume that A8: e1 in dom (f * g) and A9: e2 in dom (f * g) ; ::_thesis: ( not e1 < e2 or (f * g) . e1 > (f * g) . e2 ) A10: e1 in dom g by A8, FUNCT_1:11; then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13; A12: e2 in dom g by A9, FUNCT_1:11; then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13; assume e1 < e2 ; ::_thesis: (f * g) . e1 > (f * g) . e2 then A14: g . e1 < g . e2 by A10, A12, Def13; ( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11; hence (f * g) . e1 > (f * g) . e2 by A11, A13, A14, Def14; ::_thesis: verum end; end; registration let f be ext-real-valued non-increasing Function; let g be ext-real-valued non-decreasing Function; clusterf * g -> non-increasing ; coherence g * f is non-increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds (g * f) . e1 >= (g * f) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 >= (g * f) . e2 ) assume that A1: e1 in dom (g * f) and A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 >= (g * f) . e2 ) A3: e1 in dom f by A1, FUNCT_1:11; then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13; A5: e2 in dom f by A2, FUNCT_1:11; then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13; assume e1 <= e2 ; ::_thesis: (g * f) . e1 >= (g * f) . e2 then A7: f . e1 >= f . e2 by A3, A5, Def16; ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11; hence (g * f) . e1 >= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum end; clusterg * f -> non-increasing ; coherence f * g is non-increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 holds (f * g) . e1 >= (f * g) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 implies (f * g) . e1 >= (f * g) . e2 ) assume that A8: e1 in dom (f * g) and A9: e2 in dom (f * g) ; ::_thesis: ( not e1 <= e2 or (f * g) . e1 >= (f * g) . e2 ) A10: e1 in dom g by A8, FUNCT_1:11; then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13; A12: e2 in dom g by A9, FUNCT_1:11; then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13; assume e1 <= e2 ; ::_thesis: (f * g) . e1 >= (f * g) . e2 then A14: g . e1 <= g . e2 by A10, A12, Def15; ( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11; hence (f * g) . e1 >= (f * g) . e2 by A11, A13, A14, Def16; ::_thesis: verum end; end; registration let X be ext-real-membered set ; cluster id X -> increasing for Function of X,X; coherence for b1 being Function of X,X st b1 = id X holds b1 is increasing proof id X is increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (id X) & e2 in dom (id X) & e1 < e2 holds (id X) . e1 < (id X) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom (id X) & e2 in dom (id X) & e1 < e2 implies (id X) . e1 < (id X) . e2 ) assume that A1: e1 in dom (id X) and A2: e2 in dom (id X) ; ::_thesis: ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) (id X) . e1 = e1 by A1, FUNCT_1:18; hence ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) by A2, FUNCT_1:18; ::_thesis: verum end; hence for b1 being Function of X,X st b1 = id X holds b1 is increasing ; ::_thesis: verum end; end; registration cluster non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing for Element of bool [:NAT,NAT:]; existence ex b1 being sequence of NAT st b1 is increasing proof take id NAT ; ::_thesis: id NAT is increasing thus id NAT is increasing ; ::_thesis: verum end; end; definition let s be ManySortedSet of NAT ; mode subsequence of s -> ManySortedSet of NAT means :Def17: :: VALUED_0:def 17 ex N being increasing sequence of NAT st it = s * N; existence ex b1 being ManySortedSet of NAT ex N being increasing sequence of NAT st b1 = s * N proof take s ; ::_thesis: ex N being increasing sequence of NAT st s = s * N take id NAT ; ::_thesis: s = s * (id NAT) dom s = NAT by PARTFUN1:def_2; hence s = s * (id NAT) by RELAT_1:52; ::_thesis: verum end; end; :: deftheorem Def17 defines subsequence VALUED_0:def_17_:_ for s, b2 being ManySortedSet of NAT holds ( b2 is subsequence of s iff ex N being increasing sequence of NAT st b2 = s * N ); Lm1: for x being non empty set for M being ManySortedSet of NAT for s being subsequence of M holds rng s c= rng M proof let x be non empty set ; ::_thesis: for M being ManySortedSet of NAT for s being subsequence of M holds rng s c= rng M let M be ManySortedSet of NAT ; ::_thesis: for s being subsequence of M holds rng s c= rng M let s be subsequence of M; ::_thesis: rng s c= rng M ex N being increasing sequence of NAT st s = M * N by Def17; hence rng s c= rng M by RELAT_1:26; ::_thesis: verum end; registration let X be non empty set ; let s be X -valued ManySortedSet of NAT ; cluster -> X -valued for subsequence of s; coherence for b1 being subsequence of s holds b1 is X -valued proof let ss be subsequence of s; ::_thesis: ss is X -valued rng ss c= rng s by Lm1; hence rng ss c= X by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; end; definition let X be non empty set ; let s be sequence of X; :: original: subsequence redefine mode subsequence of s -> sequence of X; coherence for b1 being subsequence of s holds b1 is sequence of X proof let ss be subsequence of s; ::_thesis: ss is sequence of X ( rng ss c= X & dom ss = NAT ) by PARTFUN1:def_2; hence ss is sequence of X by RELSET_1:4; ::_thesis: verum end; end; definition let X be non empty set ; let s be sequence of X; let k be Nat; :: original: ^\ redefine funcs ^\ k -> subsequence of s; coherence s ^\ k is subsequence of s proof set N = (id NAT) ^\ k; (id NAT) ^\ k is increasing proof let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 holds ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 let e2 be ext-real number ; ::_thesis: ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 implies ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 ) assume ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) ) ; ::_thesis: ( not e1 < e2 or ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 ) then reconsider i = e1, j = e2 as Element of NAT ; A1: ((id NAT) ^\ k) . j = (id NAT) . (j + k) by NAT_1:def_3 .= j + k by FUNCT_1:18 ; assume A2: e1 < e2 ; ::_thesis: ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 ((id NAT) ^\ k) . i = (id NAT) . (i + k) by NAT_1:def_3 .= i + k by FUNCT_1:18 ; hence ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 by A1, A2, XREAL_1:6; ::_thesis: verum end; then reconsider N = (id NAT) ^\ k as increasing sequence of NAT ; thus s ^\ k is subsequence of s ::_thesis: verum proof take N ; :: according to VALUED_0:def_17 ::_thesis: s ^\ k = s * N thus s ^\ k = (s * (id NAT)) ^\ k by FUNCT_2:17 .= s * N by NAT_1:50 ; ::_thesis: verum end; end; end; theorem :: VALUED_0:19 for XX being non empty set for ss being sequence of XX holds ss is subsequence of ss proof let XX be non empty set ; ::_thesis: for ss being sequence of XX holds ss is subsequence of ss let ss be sequence of XX; ::_thesis: ss is subsequence of ss take id NAT ; :: according to VALUED_0:def_17 ::_thesis: ss = ss * (id NAT) thus ss = ss * (id NAT) by FUNCT_2:17; ::_thesis: verum end; theorem :: VALUED_0:20 for XX being non empty set for ss1, ss2, ss3 being sequence of XX st ss1 is subsequence of ss2 & ss2 is subsequence of ss3 holds ss1 is subsequence of ss3 proof let XX be non empty set ; ::_thesis: for ss1, ss2, ss3 being sequence of XX st ss1 is subsequence of ss2 & ss2 is subsequence of ss3 holds ss1 is subsequence of ss3 let ss1, ss2, ss3 be sequence of XX; ::_thesis: ( ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies ss1 is subsequence of ss3 ) given N1 being increasing sequence of NAT such that A1: ss1 = ss2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ( not ss2 is subsequence of ss3 or ss1 is subsequence of ss3 ) given N2 being increasing sequence of NAT such that A2: ss2 = ss3 * N2 ; :: according to VALUED_0:def_17 ::_thesis: ss1 is subsequence of ss3 take N2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ss1 = ss3 * (N2 * N1) thus ss1 = ss3 * (N2 * N1) by A1, A2, RELAT_1:36; ::_thesis: verum end; registration let X be set ; cluster Relation-like NAT -defined X -valued Function-like constant quasi_total for Element of bool [:NAT,X:]; existence ex b1 being sequence of X st b1 is constant proof percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: ex b1 being sequence of X st b1 is constant then reconsider s = {} as sequence of X by FUNCT_2:def_1, RELSET_1:12; take s ; ::_thesis: s is constant thus s is constant ; ::_thesis: verum end; suppose X <> {} ; ::_thesis: ex b1 being sequence of X st b1 is constant then consider x being set such that A1: x in X by XBOOLE_0:def_1; reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45; take s ; ::_thesis: s is constant thus s is constant ; ::_thesis: verum end; end; end; end; theorem Th21: :: VALUED_0:21 for XX being non empty set for ss being sequence of XX for ss1 being subsequence of ss holds rng ss1 c= rng ss proof let XX be non empty set ; ::_thesis: for ss being sequence of XX for ss1 being subsequence of ss holds rng ss1 c= rng ss let ss be sequence of XX; ::_thesis: for ss1 being subsequence of ss holds rng ss1 c= rng ss let ss1 be subsequence of ss; ::_thesis: rng ss1 c= rng ss let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ss1 or x in rng ss ) consider N being increasing sequence of NAT such that A1: ss1 = ss * N by Def17; assume x in rng ss1 ; ::_thesis: x in rng ss then consider n being set such that A2: n in NAT and A3: x = ss1 . n by FUNCT_2:11; A4: N . n in NAT by A2, FUNCT_2:5; x = ss . (N . n) by A1, A2, A3, FUNCT_2:15; hence x in rng ss by A4, FUNCT_2:4; ::_thesis: verum end; registration let X be non empty set ; let s be constant sequence of X; cluster -> constant for subsequence of s; coherence for b1 being subsequence of s holds b1 is constant proof let s1 be subsequence of s; ::_thesis: s1 is constant rng s1 c= rng s by Th21; hence s1 is constant ; ::_thesis: verum end; end; definition let X be non empty set ; let N be increasing sequence of NAT; let s be sequence of X; :: original: * redefine funcs * N -> subsequence of s; correctness coherence N * s is subsequence of s; by Def17; end; theorem :: VALUED_0:22 for X, Y being non empty set for s, s1 being sequence of X for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds h /* s1 is subsequence of h /* s proof let X, Y be non empty set ; ::_thesis: for s, s1 being sequence of X for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds h /* s1 is subsequence of h /* s let s, s1 be sequence of X; ::_thesis: for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds h /* s1 is subsequence of h /* s let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h & s1 is subsequence of s implies h /* s1 is subsequence of h /* s ) assume that A1: rng s c= dom h and A2: s1 is subsequence of s ; ::_thesis: h /* s1 is subsequence of h /* s consider N being increasing sequence of NAT such that A3: s1 = s * N by A2, Def17; take N ; :: according to VALUED_0:def_17 ::_thesis: h /* s1 = (h /* s) * N thus h /* s1 = (h /* s) * N by A1, A3, FUNCT_2:110; ::_thesis: verum end; registration let X be with_non-empty_element set ; cluster non empty Relation-like non-empty NAT -defined X -valued Function-like total quasi_total for Element of bool [:NAT,X:]; existence ex b1 being sequence of X st b1 is non-empty proof consider x being non empty set such that A1: x in X by SETFAM_1:def_10; reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45; take s ; ::_thesis: s is non-empty thus s is non-empty ; ::_thesis: verum end; end; registration let X be with_non-empty_element set ; let s be non-empty sequence of X; cluster -> non-empty for subsequence of s; coherence for b1 being subsequence of s holds b1 is non-empty proof let s1 be subsequence of s; ::_thesis: s1 is non-empty rng s1 c= rng s by Th21; hence not {} in rng s1 ; :: according to RELAT_1:def_9 ::_thesis: verum end; end; definition let X be non empty set ; let s be sequence of X; :: original: constant redefine attrs is constant means :: VALUED_0:def 18 ex x being Element of X st for n being Nat holds s . n = x; compatibility ( s is constant iff ex x being Element of X st for n being Nat holds s . n = x ) proof hereby ::_thesis: ( ex x being Element of X st for n being Nat holds s . n = x implies s is constant ) assume s is constant ; ::_thesis: ex x being Element of X st for n being Nat holds s . n = x then consider x being Element of X such that A1: for n being Element of NAT st n in dom s holds s . n = x by PARTFUN2:def_1; take x = x; ::_thesis: for n being Nat holds s . n = x let n be Nat; ::_thesis: s . n = x ( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12; hence s . n = x by A1; ::_thesis: verum end; given x being Element of X such that A2: for n being Nat holds s . n = x ; ::_thesis: s is constant take x ; :: according to PARTFUN2:def_1 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom s or s . b1 = x ) thus for b1 being Element of NAT holds ( not b1 in dom s or s . b1 = x ) by A2; ::_thesis: verum end; end; :: deftheorem defines constant VALUED_0:def_18_:_ for X being non empty set for s being sequence of X holds ( s is constant iff ex x being Element of X st for n being Nat holds s . n = x ); theorem Th23: :: VALUED_0:23 for i, j being Nat for X being set for s being constant sequence of X holds s . i = s . j proof let i, j be Nat; ::_thesis: for X being set for s being constant sequence of X holds s . i = s . j let X be set ; ::_thesis: for s being constant sequence of X holds s . i = s . j let s be constant sequence of X; ::_thesis: s . i = s . j percases ( X is empty or not X is empty ) ; supposeA1: X is empty ; ::_thesis: s . i = s . j then s . i = {} ; hence s . i = s . j by A1; ::_thesis: verum end; suppose not X is empty ; ::_thesis: s . i = s . j then dom s = NAT by FUNCT_2:def_1; then ( i in dom s & j in dom s ) by ORDINAL1:def_12; hence s . i = s . j by FUNCT_1:def_10; ::_thesis: verum end; end; end; theorem Th24: :: VALUED_0:24 for X being non empty set for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds s is V29() proof let X be non empty set ; ::_thesis: for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds s is V29() let s be sequence of X; ::_thesis: ( ( for i, j being Nat holds s . i = s . j ) implies s is V29() ) assume for i, j being Nat holds s . i = s . j ; ::_thesis: s is V29() then for x, y being set st x in dom s & y in dom s holds s . x = s . y ; hence s is V29() by FUNCT_1:def_10; ::_thesis: verum end; theorem :: VALUED_0:25 for X being non empty set for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds s is V29() proof let X be non empty set ; ::_thesis: for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds s is V29() let s be sequence of X; ::_thesis: ( ( for i being Nat holds s . i = s . (i + 1) ) implies s is V29() ) assume A1: for i being Nat holds s . i = s . (i + 1) ; ::_thesis: s is V29() now__::_thesis:_for_i,_j_being_Nat_holds_s_._i_=_s_._j let i, j be Nat; ::_thesis: s . i = s . j A2: now__::_thesis:_for_i,_j_being_Nat_st_i_<=_j_holds_ s_._i_=_s_._j let i, j be Nat; ::_thesis: ( i <= j implies s . i = s . j ) assume A3: i <= j ; ::_thesis: s . i = s . j defpred S1[ Nat] means ( i <= \$1 implies s . i = s . \$1 ); A4: for j being Nat st S1[j] holds S1[j + 1] proof let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] ) assume A5: S1[j] ; ::_thesis: S1[j + 1] assume i <= j + 1 ; ::_thesis: s . i = s . (j + 1) then ( i < j + 1 or i = j + 1 ) by XXREAL_0:1; hence s . i = s . (j + 1) by A1, A5, NAT_1:13; ::_thesis: verum end; A6: S1[ 0 ] by NAT_1:3; for j being Nat holds S1[j] from NAT_1:sch_2(A6, A4); hence s . i = s . j by A3; ::_thesis: verum end; ( i <= j or j <= i ) ; hence s . i = s . j by A2; ::_thesis: verum end; hence s is V29() by Th24; ::_thesis: verum end; theorem :: VALUED_0:26 for X being non empty set for s, s1 being sequence of X st s is V29() & s1 is subsequence of s holds s = s1 proof let X be non empty set ; ::_thesis: for s, s1 being sequence of X st s is V29() & s1 is subsequence of s holds s = s1 let s, s1 be sequence of X; ::_thesis: ( s is V29() & s1 is subsequence of s implies s = s1 ) assume that A1: s is V29() and A2: s1 is subsequence of s ; ::_thesis: s = s1 let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: s . n = s1 . n consider N being increasing sequence of NAT such that A3: s1 = s * N by A2, Def17; thus s1 . n = s . (N . n) by A3, FUNCT_2:15 .= s . n by A1, Th23 ; ::_thesis: verum end; theorem Th27: :: VALUED_0:27 for X, Y being non empty set for s being sequence of X for h being PartFunc of X,Y for n being Nat st rng s c= dom h holds (h /* s) ^\ n = h /* (s ^\ n) proof let X, Y be non empty set ; ::_thesis: for s being sequence of X for h being PartFunc of X,Y for n being Nat st rng s c= dom h holds (h /* s) ^\ n = h /* (s ^\ n) let s be sequence of X; ::_thesis: for h being PartFunc of X,Y for n being Nat st rng s c= dom h holds (h /* s) ^\ n = h /* (s ^\ n) let h be PartFunc of X,Y; ::_thesis: for n being Nat st rng s c= dom h holds (h /* s) ^\ n = h /* (s ^\ n) let n be Nat; ::_thesis: ( rng s c= dom h implies (h /* s) ^\ n = h /* (s ^\ n) ) assume A1: rng s c= dom h ; ::_thesis: (h /* s) ^\ n = h /* (s ^\ n) let m be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((h /* s) ^\ n) . m = (h /* (s ^\ n)) . m A2: rng (s ^\ n) c= rng s by Th21; thus ((h /* s) ^\ n) . m = (h /* s) . (m + n) by NAT_1:def_3 .= h . (s . (m + n)) by A1, FUNCT_2:108 .= h . ((s ^\ n) . m) by NAT_1:def_3 .= (h /* (s ^\ n)) . m by A1, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum end; theorem Th28: :: VALUED_0:28 for X being non empty set for s being sequence of X for n being Nat holds s . n in rng s proof let X be non empty set ; ::_thesis: for s being sequence of X for n being Nat holds s . n in rng s let s be sequence of X; ::_thesis: for n being Nat holds s . n in rng s let n be Nat; ::_thesis: s . n in rng s n in NAT by ORDINAL1:def_12; hence s . n in rng s by FUNCT_2:112; ::_thesis: verum end; theorem :: VALUED_0:29 for X, Y being non empty set for s being sequence of X for h being PartFunc of X,Y for n being Nat st h is total holds h /* (s ^\ n) = (h /* s) ^\ n proof let X, Y be non empty set ; ::_thesis: for s being sequence of X for h being PartFunc of X,Y for n being Nat st h is total holds h /* (s ^\ n) = (h /* s) ^\ n let s be sequence of X; ::_thesis: for h being PartFunc of X,Y for n being Nat st h is total holds h /* (s ^\ n) = (h /* s) ^\ n let h be PartFunc of X,Y; ::_thesis: for n being Nat st h is total holds h /* (s ^\ n) = (h /* s) ^\ n let n be Nat; ::_thesis: ( h is total implies h /* (s ^\ n) = (h /* s) ^\ n ) assume h is total ; ::_thesis: h /* (s ^\ n) = (h /* s) ^\ n then dom h = X by PARTFUN1:def_2; then rng s c= dom h ; hence h /* (s ^\ n) = (h /* s) ^\ n by Th27; ::_thesis: verum end; theorem Th30: :: VALUED_0:30 for X, Y being non empty set for s being sequence of X for h being PartFunc of X,Y st rng s c= dom h holds h .: (rng s) = rng (h /* s) proof let X, Y be non empty set ; ::_thesis: for s being sequence of X for h being PartFunc of X,Y st rng s c= dom h holds h .: (rng s) = rng (h /* s) let s be sequence of X; ::_thesis: for h being PartFunc of X,Y st rng s c= dom h holds h .: (rng s) = rng (h /* s) let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h implies h .: (rng s) = rng (h /* s) ) assume A1: rng s c= dom h ; ::_thesis: h .: (rng s) = rng (h /* s) now__::_thesis:_for_r_being_Element_of_Y_holds_ (_(_r_in_h_.:_(rng_s)_implies_r_in_rng_(h_/*_s)_)_&_(_r_in_rng_(h_/*_s)_implies_r_in_h_.:_(rng_s)_)_) let r be Element of Y; ::_thesis: ( ( r in h .: (rng s) implies r in rng (h /* s) ) & ( r in rng (h /* s) implies r in h .: (rng s) ) ) thus ( r in h .: (rng s) implies r in rng (h /* s) ) ::_thesis: ( r in rng (h /* s) implies r in h .: (rng s) ) proof assume r in h .: (rng s) ; ::_thesis: r in rng (h /* s) then consider p being Element of X such that p in dom h and A2: p in rng s and A3: r = h . p by PARTFUN2:59; consider n being Element of NAT such that A4: p = s . n by A2, FUNCT_2:113; r = (h /* s) . n by A1, A3, A4, FUNCT_2:108; hence r in rng (h /* s) by Th28; ::_thesis: verum end; assume r in rng (h /* s) ; ::_thesis: r in h .: (rng s) then consider n being Element of NAT such that A5: (h /* s) . n = r by FUNCT_2:113; A6: s . n in rng s by Th28; r = h . (s . n) by A1, A5, FUNCT_2:108; hence r in h .: (rng s) by A1, A6, FUNCT_1:def_6; ::_thesis: verum end; hence h .: (rng s) = rng (h /* s) by SUBSET_1:3; ::_thesis: verum end; theorem :: VALUED_0:31 for X, Y being non empty set for Z being set for s being sequence of X for h1 being PartFunc of X,Y for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds h2 /* (h1 /* s) = (h2 * h1) /* s proof let X, Y be non empty set ; ::_thesis: for Z being set for s being sequence of X for h1 being PartFunc of X,Y for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds h2 /* (h1 /* s) = (h2 * h1) /* s let Z be set ; ::_thesis: for s being sequence of X for h1 being PartFunc of X,Y for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds h2 /* (h1 /* s) = (h2 * h1) /* s let s be sequence of X; ::_thesis: for h1 being PartFunc of X,Y for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds h2 /* (h1 /* s) = (h2 * h1) /* s let h1 be PartFunc of X,Y; ::_thesis: for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds h2 /* (h1 /* s) = (h2 * h1) /* s let h2 be PartFunc of Y,Z; ::_thesis: ( rng s c= dom (h2 * h1) implies h2 /* (h1 /* s) = (h2 * h1) /* s ) assume A1: rng s c= dom (h2 * h1) ; ::_thesis: h2 /* (h1 /* s) = (h2 * h1) /* s now__::_thesis:_for_n_being_Element_of_NAT_holds_((h2_*_h1)_/*_s)_._n_=_(h2_/*_(h1_/*_s))_._n let n be Element of NAT ; ::_thesis: ((h2 * h1) /* s) . n = (h2 /* (h1 /* s)) . n A2: rng s c= dom h1 by A1, FUNCT_1:101; h1 .: (rng s) c= dom h2 by A1, FUNCT_1:101; then A3: rng (h1 /* s) c= dom h2 by A2, Th30; s . n in rng s by Th28; then A4: s . n in dom h1 by A1, FUNCT_1:11; thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:108 .= h2 . (h1 . (s . n)) by A4, FUNCT_1:13 .= h2 . ((h1 /* s) . n) by A2, FUNCT_2:108 .= (h2 /* (h1 /* s)) . n by A3, FUNCT_2:108 ; ::_thesis: verum end; hence h2 /* (h1 /* s) = (h2 * h1) /* s by FUNCT_2:63; ::_thesis: verum end; definition let f be ext-real-valued Function; attrf is zeroed means :: VALUED_0:def 19 f . {} = 0 ; end; :: deftheorem defines zeroed VALUED_0:def_19_:_ for f being ext-real-valued Function holds ( f is zeroed iff f . {} = 0 ); registration cluster Relation-like COMPLEX -valued -> complex-valued for set ; coherence for b1 being Relation st b1 is COMPLEX -valued holds b1 is complex-valued proof let R be Relation; ::_thesis: ( R is COMPLEX -valued implies R is complex-valued ) assume R is COMPLEX -valued ; ::_thesis: R is complex-valued hence rng R c= COMPLEX by RELAT_1:def_19; :: according to VALUED_0:def_1 ::_thesis: verum end; cluster Relation-like ExtREAL -valued -> ext-real-valued for set ; coherence for b1 being Relation st b1 is ExtREAL -valued holds b1 is ext-real-valued proof let R be Relation; ::_thesis: ( R is ExtREAL -valued implies R is ext-real-valued ) assume R is ExtREAL -valued ; ::_thesis: R is ext-real-valued hence rng R c= ExtREAL by RELAT_1:def_19; :: according to VALUED_0:def_2 ::_thesis: verum end; cluster Relation-like REAL -valued -> real-valued for set ; coherence for b1 being Relation st b1 is REAL -valued holds b1 is real-valued proof let R be Relation; ::_thesis: ( R is REAL -valued implies R is real-valued ) assume R is REAL -valued ; ::_thesis: R is real-valued hence rng R c= REAL by RELAT_1:def_19; :: according to VALUED_0:def_3 ::_thesis: verum end; cluster Relation-like NAT -valued -> natural-valued for set ; coherence for b1 being Relation st b1 is NAT -valued holds b1 is natural-valued proof let R be Relation; ::_thesis: ( R is NAT -valued implies R is natural-valued ) assume R is NAT -valued ; ::_thesis: R is natural-valued hence rng R c= NAT by RELAT_1:def_19; :: according to VALUED_0:def_6 ::_thesis: verum end; end; definition let s be ManySortedSet of NAT ; redefine attr s is constant means :: VALUED_0:def 20 ex x being set st for n being Nat holds s . n = x; compatibility ( s is constant iff ex x being set st for n being Nat holds s . n = x ) proof A1: dom s = NAT by PARTFUN1:def_2; hereby ::_thesis: ( ex x being set st for n being Nat holds s . n = x implies s is constant ) assume A2: s is constant ; ::_thesis: ex x being set st for n being Nat holds s . n = x take x = s . 0; ::_thesis: for n being Nat holds s . n = x let n be Nat; ::_thesis: s . n = x ( 0 in dom s & n in dom s ) by A1, ORDINAL1:def_12; hence s . n = x by A2, FUNCT_1:def_10; ::_thesis: verum end; given x being set such that A3: for n being Nat holds s . n = x ; ::_thesis: s is constant let n1, n2 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not n1 in dom s or not n2 in dom s or s . n1 = s . n2 ) assume A4: ( n1 in dom s & n2 in dom s ) ; ::_thesis: s . n1 = s . n2 hence s . n1 = x by A3 .= s . n2 by A3, A4 ; ::_thesis: verum end; end; :: deftheorem defines constant VALUED_0:def_20_:_ for s being ManySortedSet of NAT holds ( s is constant iff ex x being set st for n being Nat holds s . n = x ); theorem :: VALUED_0:32 for x being non empty set for M being ManySortedSet of NAT for s being subsequence of M holds rng s c= rng M by Lm1; registration let X be set ; cluster Relation-like X -defined Function-like total natural-valued for set ; existence ex b1 being ManySortedSet of X st b1 is natural-valued proof take X --> 0 ; ::_thesis: X --> 0 is natural-valued thus X --> 0 is natural-valued ; ::_thesis: verum end; end;