:: Properties of Number-Valued Functions :: by Library Committee :: :: Received December 18, 2007 :: Copyright (c) 2007-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, ORDINAL1, XXREAL_0, VALUED_0, RAT_1, COMPLEX1, ARYTM_1, ARYTM_3, MEMBERED, PARTFUN1, TARSKI, SUBSET_1, CARD_1, XCMPLX_0, INT_1, SQUARE_1, FUNCT_4, FINSET_1, NAT_1, ORDINAL2, VALUED_1, AMISTD_1, FUNCOP_1, AMISTD_2, AMISTD_3, ORDINAL4, REAL_1, XREAL_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, XCMPLX_0, NUMBERS, COMPLEX1, XXREAL_0, XXREAL_2, FUNCOP_1, XREAL_0, RAT_1, INT_1, INT_2, SQUARE_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FINSEQ_1, MEMBERED, NAT_1, VALUED_0; constructors PARTFUN1, RAT_1, VALUED_0, SQUARE_1, MEMBERED, INT_2, FINSEQ_1, NAT_1, FUNCT_4, NAT_D, RELSET_1, XXREAL_2, FUNCOP_1, DOMAIN_1, WELLORD2, FINSEQ_3, REAL_1; registrations ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RAT_1, INT_1, NAT_1, FUNCT_1, FINSET_1, XXREAL_0, RELAT_1, XXREAL_2, FUNCOP_1, FUNCT_4, CARD_1, FINSEQ_1; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0, WELLORD2; equalities XBOOLE_0, XCMPLX_0, SQUARE_1, FINSEQ_1, FUNCOP_1; expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, VALUED_0, WELLORD2; theorems FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, VALUED_0, COMPLEX1, FINSEQ_1, XBOOLE_0, TARSKI, GRFUNC_1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, INT_1, ORDINAL1, XXREAL_0, FUNCOP_1, ZFMISC_1, XXREAL_2, XBOOLE_1, CARD_1, CARD_2, RAT_1, XTUPLE_0, XREAL_1, FINSEQ_3; schemes FUNCT_1, CLASSES1, FRAENKEL, RECDEF_1, NAT_1; begin :: f1 + f2 Lm1: for f being FinSequence, h being Function st dom h = dom f holds h is FinSequence proof let f be FinSequence, h be Function such that A1: dom h = dom f; h is FinSequence-like proof take len f; thus thesis by A1,FINSEQ_1:def 3; end; hence thesis; end; Lm2: for f, g being FinSequence, h being Function st dom h = dom f /\ dom g holds h is FinSequence proof let f, g be FinSequence, h be Function such that A1: dom h = dom f /\ dom g; consider n being Nat such that A2: dom f = Seg n by FINSEQ_1:def 2; consider m being Nat such that A3: dom g = Seg m by FINSEQ_1:def 2; h is FinSequence-like proof per cases; suppose A4: n <= m; take n; thus thesis by A1,A2,A3,A4,FINSEQ_1:7; end; suppose A5: m <= n; take m; thus thesis by A1,A2,A3,A5,FINSEQ_1:7; end; end; hence thesis; end; registration cluster complex-valued for FinSequence; existence proof take <*>COMPLEX; thus thesis; end; end; :: move somewhere registration let r be Rational; cluster |. r .| -> rational; coherence proof |. r .| = -r or |. r .| = r by COMPLEX1:71; hence thesis; end; end; definition let f1,f2 be complex-valued Function; deffunc F(object) = f1.$1 + f2.$1; set X = dom f1 /\ dom f2; func f1 + f2 -> Function means :Def1: dom it = dom f1 /\ dom f2 & for c being object st c in dom it holds it.c = f1.c + f2.c; existence proof ex f being Function st dom f = X & for x being object st x in X holds f.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let f, g be Function such that A1: dom f = X and A2: for c being object st c in dom f holds f.c = F(c) and A3: dom g = X and A4: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A5: x in dom f; hence f.x = F(x) by A2 .= g.x by A1,A3,A4,A5; end; hence thesis by A1,A3; end; commutativity; end; registration let f1,f2 be complex-valued Function; cluster f1+f2 -> complex-valued; coherence proof let x be object; assume x in dom (f1+f2); then (f1+f2).x = f1.x + f2.x by Def1; hence thesis; end; end; registration let f1,f2 be real-valued Function; cluster f1+f2 -> real-valued; coherence proof let x be object; assume x in dom (f1+f2); then (f1+f2).x = f1.x + f2.x by Def1; hence thesis; end; end; registration let f1,f2 be RAT-valued Function; cluster f1+f2 -> RAT-valued; coherence proof let y be object; assume y in rng(f1+f2); then consider x being object such that A1: x in dom (f1+f2) and A2: (f1+f2).x = y by FUNCT_1:def 3; (f1+f2).x = f1.x + f2.x by A1,Def1; hence thesis by A2,RAT_1:def 2; end; end; registration let f1,f2 be INT-valued Function; cluster f1+f2 -> INT-valued; coherence proof let y be object; assume y in rng(f1+f2); then consider x being object such that A1: x in dom (f1+f2) and A2: (f1+f2).x = y by FUNCT_1:def 3; (f1+f2).x = f1.x + f2.x by A1,Def1; hence thesis by A2,INT_1:def 2; end; end; registration let f1,f2 be natural-valued Function; cluster f1+f2 -> natural-valued; coherence proof let x be object; assume x in dom (f1+f2); then (f1+f2).x = f1.x + f2.x by Def1; hence thesis; end; end; definition let C be set; let D1,D2 be complex-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1+f2 -> PartFunc of C,COMPLEX; coherence proof dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= COMPLEX by Def1, VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be real-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1+f2 -> PartFunc of C,REAL; coherence proof dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= REAL by Def1,VALUED_0:def 3 ; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be rational-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1+f2 -> PartFunc of C,RAT; coherence proof dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= RAT by Def1,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be integer-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1+f2 -> PartFunc of C,INT; coherence proof dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= INT by Def1,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be natural-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1+f2 -> PartFunc of C,NAT; coherence proof dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= NAT by Def1,VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; registration let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1+f2 -> total for PartFunc of C,COMPLEX; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1+f2) = C /\ C by Def1 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be real-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1+f2 -> total for PartFunc of C,REAL; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1+f2) = C /\ C by Def1 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be rational-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1+f2 -> total for PartFunc of C,RAT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1+f2) = C /\ C by Def1 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be integer-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1+f2 -> total for PartFunc of C,INT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1+f2) = C /\ C by Def1 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be natural-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1+f2 -> total for PartFunc of C,NAT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1+f2) = C /\ C by Def1 .= C; hence thesis by PARTFUN1:def 2; end; end; theorem for C being set, D1,D2 being complex-membered non empty set for f1 being Function of C,D1, f2 being Function of C,D2 for c being Element of C holds (f1+f2).c = f1.c + f2.c proof let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1, f2 be Function of C,D2; A1: dom(f1+f2) = C by FUNCT_2:def 1; let c be Element of C; per cases; suppose C is non empty; hence thesis by A1,Def1; end; suppose A2: C is empty; then f1.c = 0; hence thesis by A2; end; end; registration let f1, f2 be complex-valued FinSequence; cluster f1+f2 -> FinSequence-like; coherence proof dom(f1+f2) = dom f1 /\ dom f2 by Def1; hence thesis by Lm2; end; end; begin :: r + f definition let f be complex-valued Function, r be Complex; deffunc F(object) = r + f.$1; func r + f -> Function means :Def2: dom it = dom f & for c being object st c in dom it holds it.c = r + f.c; existence proof ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let h, g be Function such that A1: dom h = dom f and A2: for c being object st c in dom h holds h.c = F(c) and A3: dom g = dom f and A4: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A5: x in dom h; hence h.x = F(x) by A2 .= g.x by A1,A3,A4,A5; end; hence thesis by A1,A3; end; end; notation let f be complex-valued Function, r be Complex; synonym f + r for r + f; end; registration let f be complex-valued Function, r be Complex; cluster r+f -> complex-valued; coherence proof let x be object; assume x in dom (r+f); then (r+f).x = r + f.x by Def2; hence thesis; end; end; registration let f be real-valued Function, r be Real; cluster r+f -> real-valued; coherence proof let x be object; assume x in dom (r+f); then (r+f).x = r + f.x by Def2; hence thesis; end; end; registration let f be RAT-valued Function, r be Rational; cluster r+f -> RAT-valued; coherence proof let y be object; assume y in rng (r+f); then consider x being object such that A1: x in dom (r+f) and A2: (r+f).x = y by FUNCT_1:def 3; (r+f).x = r + f.x by A1,Def2; hence thesis by A2,RAT_1:def 2; end; end; registration let f be INT-valued Function, r be Integer; cluster r+f -> INT-valued; coherence proof let y be object; assume y in rng (r+f); then consider x being object such that A1: x in dom (r+f) and A2: (r+f).x = y by FUNCT_1:def 3; (r+f).x = r + f.x by A1,Def2; hence thesis by A2,INT_1:def 2; end; end; registration let f be natural-valued Function, r be Nat; cluster r+f -> natural-valued; coherence proof let x be object; assume x in dom (r+f); then (r+f).x = r + f.x by Def2; hence thesis; end; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; let r be Complex; redefine func r+f -> PartFunc of C,COMPLEX; coherence proof dom (r+f) = dom f & rng (r+f) c= COMPLEX by Def2,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; let r be Real; redefine func r+f -> PartFunc of C,REAL; coherence proof dom (r+f) = dom f & rng (r+f) c= REAL by Def2,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; let r be Rational; redefine func r+f -> PartFunc of C,RAT; coherence proof dom (r+f) = dom f & rng (r+f) c= RAT by Def2,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; let r be Integer; redefine func r+f -> PartFunc of C,INT; coherence proof dom (r+f) = dom f & rng (r+f) c= INT by Def2,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be natural-membered set; let f be PartFunc of C,D; let r be Nat; redefine func r+f -> PartFunc of C,NAT; coherence proof dom (r+f) = dom f & rng (r+f) c= NAT by Def2,VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; let r be Complex; cluster r+f -> total for PartFunc of C,COMPLEX; coherence proof dom(r+f) = dom f by Def2 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; let r be Real; cluster r+f -> total for PartFunc of C,REAL; coherence proof dom(r+f) = dom f by Def2 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; let r be Rational; cluster r+f -> total for PartFunc of C,RAT; coherence proof dom(r+f) = dom f by Def2 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; let r be Integer; cluster r+f -> total for PartFunc of C,INT; coherence proof dom(r+f) = dom f by Def2 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be natural-membered non empty set; let f be Function of C,D; let r be Nat; cluster r+f -> total for PartFunc of C,NAT; coherence proof dom(r+f) = dom f by Def2 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; theorem for C being non empty set, D being complex-membered non empty set for f being Function of C,D, r being Complex for c being Element of C holds (r+f).c = r + f.c proof let C be non empty set; let D be complex-membered non empty set; let f be Function of C,D, r be Complex; dom(r+f) = C by FUNCT_2:def 1; hence thesis by Def2; end; registration let f be complex-valued FinSequence, r be Complex; cluster r+f -> FinSequence-like; coherence proof dom (r+f) = dom f by Def2; hence thesis by Lm1; end; end; begin :: f - r definition let f be complex-valued Function, r be Complex; func f - r -> Function equals -r + f; coherence; end; theorem for f being complex-valued Function, r being Complex holds dom (f-r) = dom f & for c being object st c in dom f holds (f-r).c = f.c - r proof let f be complex-valued Function, r be Complex; dom (f-r) = dom f by Def2; hence thesis by Def2; end; registration let f be complex-valued Function, r be Complex; cluster f-r -> complex-valued; coherence; end; registration let f be real-valued Function, r be Real; cluster f-r -> real-valued; coherence; end; registration let f be RAT-valued Function, r be Rational; cluster f-r -> RAT-valued; coherence; end; registration let f be INT-valued Function, r be Integer; cluster f-r -> INT-valued; coherence; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; let r be Complex; redefine func f-r -> PartFunc of C,COMPLEX; coherence proof dom (f-r) = dom f & rng (f-r) c= COMPLEX by Def2,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; let r be Real; redefine func f-r -> PartFunc of C,REAL; coherence proof dom (f-r) = dom f & rng (f-r) c= REAL by Def2,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; let r be Rational; redefine func f-r -> PartFunc of C,RAT; coherence proof dom (f-r) = dom f & rng (f-r) c= RAT by Def2,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; let r be Integer; redefine func f-r -> PartFunc of C,INT; coherence proof dom (f-r) = dom f & rng (f-r) c= INT by Def2,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; let r be Complex; cluster f-r -> total for PartFunc of C,COMPLEX; coherence; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; let r be Real; cluster f-r -> total for PartFunc of C,REAL; coherence; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; let r be Rational; cluster f-r -> total for PartFunc of C,RAT; coherence; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; let r be Integer; cluster f-r -> total for PartFunc of C,INT; coherence; end; theorem for C being non empty set, D being complex-membered non empty set for f being Function of C,D, r being Complex for c being Element of C holds (f-r).c = f.c - r proof let C be non empty set; let D be complex-membered non empty set; let f be Function of C,D, r be Complex; dom (f-r) = C by FUNCT_2:def 1; hence thesis by Def2; end; registration let f be complex-valued FinSequence, r be Complex; cluster f-r -> FinSequence-like; coherence; end; begin :: f1 (#) f2 definition let f1,f2 be complex-valued Function; deffunc F(object) = f1.$1 * f2.$1; set X = dom f1 /\ dom f2; func f1 (#) f2 -> Function means :Def4: dom it = dom f1 /\ dom f2 & for c being object st c in dom it holds it.c = f1.c * f2.c; existence proof ex f being Function st dom f = X & for x being object st x in X holds f.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let f, g be Function such that A1: dom f = X and A2: for c being object st c in dom f holds f.c = F(c) and A3: dom g = X and A4: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A5: x in dom f; hence f.x = F(x) by A2 .= g.x by A1,A3,A4,A5; end; hence thesis by A1,A3; end; commutativity; end; theorem for f1,f2 being complex-valued Function for c being object holds (f1(#)f2).c = f1.c * f2.c proof let f1,f2 be complex-valued Function; let c be object; A1: dom (f1(#)f2) = dom f1 /\ dom f2 by Def4; per cases; suppose c in dom (f1(#)f2); hence thesis by Def4; end; suppose A2: not c in dom (f1(#)f2); then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4; then f1.c = 0 or f2.c = 0 by FUNCT_1:def 2; hence thesis by A2,FUNCT_1:def 2; end; end; registration let f1,f2 be complex-valued Function; cluster f1(#)f2 -> complex-valued; coherence proof let x be object; assume x in dom (f1(#)f2); then (f1(#)f2).x = f1.x * f2.x by Def4; hence thesis; end; end; registration let f1,f2 be real-valued Function; cluster f1(#)f2 -> real-valued; coherence proof let x be object; assume x in dom (f1(#)f2); then (f1(#)f2).x = f1.x * f2.x by Def4; hence thesis; end; end; registration let f1,f2 be RAT-valued Function; cluster f1(#)f2 -> RAT-valued; coherence proof let y be object; assume y in rng (f1(#)f2); then consider x being object such that A1: x in dom (f1(#)f2) and A2: (f1(#)f2).x = y by FUNCT_1:def 3; (f1(#)f2).x = f1.x * f2.x by A1,Def4; hence thesis by A2,RAT_1:def 2; end; end; registration let f1,f2 be INT-valued Function; cluster f1(#)f2 -> INT-valued; coherence proof let y be object; assume y in rng (f1(#)f2); then consider x being object such that A1: x in dom (f1(#)f2) and A2: (f1(#)f2).x = y by FUNCT_1:def 3; (f1(#)f2).x = f1.x * f2.x by A1,Def4; hence thesis by A2,INT_1:def 2; end; end; registration let f1,f2 be natural-valued Function; cluster f1(#)f2 -> natural-valued; coherence proof let x be object; assume x in dom (f1(#)f2); then (f1(#)f2).x = f1.x * f2.x by Def4; hence thesis; end; end; definition let C be set; let D1,D2 be complex-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1(#)f2 -> PartFunc of C,COMPLEX; coherence proof dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= COMPLEX by Def4, VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be real-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1(#)f2 -> PartFunc of C,REAL; coherence proof dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= REAL by Def4, VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be rational-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1(#)f2 -> PartFunc of C,RAT; coherence proof dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= RAT by Def4, RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be integer-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1(#)f2 -> PartFunc of C,INT; coherence proof dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= INT by Def4, RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be natural-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1(#)f2 -> PartFunc of C,NAT; coherence proof dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= NAT by Def4, VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; registration let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1(#)f2 -> total for PartFunc of C,COMPLEX; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1(#)f2) = C /\ C by Def4 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be real-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1(#)f2 -> total for PartFunc of C,REAL; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1(#)f2) = C /\ C by Def4 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be rational-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1(#)f2 -> total for PartFunc of C,RAT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1(#)f2) = C /\ C by Def4 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be integer-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1(#)f2 -> total for PartFunc of C,INT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1(#)f2) = C /\ C by Def4 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D1,D2 be natural-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1(#)f2 -> total for PartFunc of C,NAT; coherence proof dom f1 = C & dom f2 = C by FUNCT_2:def 1; then dom(f1(#)f2) = C /\ C by Def4 .= C; hence thesis by PARTFUN1:def 2; end; end; registration let f1, f2 be complex-valued FinSequence; cluster f1(#)f2 -> FinSequence-like; coherence proof dom(f1(#)f2) = dom f1 /\ dom f2 by Def4; hence thesis by Lm2; end; end; begin :: r (#) f definition let f be complex-valued Function, r be Complex; deffunc F(object) = r * f.$1; func r (#) f -> Function means :Def5: dom it = dom f & for c being object st c in dom it holds it.c = r * f.c; existence proof ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let h, g be Function such that A1: dom h = dom f and A2: for c being object st c in dom h holds h.c = F(c) and A3: dom g = dom f and A4: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A5: x in dom h; hence h.x = F(x) by A2 .= g.x by A1,A3,A4,A5; end; hence thesis by A1,A3; end; end; notation let f be complex-valued Function, r be Complex; synonym f (#) r for r (#) f; end; theorem Th6: for f being complex-valued Function, r being Complex for c being object holds (r(#)f).c = r * f.c proof let f be complex-valued Function, r be Complex; let c be object; A1: dom f = dom (r(#)f) by Def5; per cases; suppose c in dom f; hence thesis by A1,Def5; end; suppose A2: not c in dom f; hence (r(#)f).c = r*0 by A1,FUNCT_1:def 2 .= r * f.c by A2,FUNCT_1:def 2; end; end; registration let f be complex-valued Function, r be Complex; cluster r(#)f -> complex-valued; coherence proof let x be object; assume x in dom (r(#)f); then (r(#)f).x = r * f.x by Def5; hence thesis; end; end; registration let f be real-valued Function, r be Real; cluster r(#)f -> real-valued; coherence proof let x be object; assume x in dom (r(#)f); then (r(#)f).x = r * f.x by Def5; hence thesis; end; end; registration let f be RAT-valued Function, r be Rational; cluster r(#)f -> RAT-valued; coherence proof let y be object; assume y in rng (r(#)f); then consider x being object such that A1: x in dom (r(#)f) and A2: (r(#)f).x = y by FUNCT_1:def 3; (r(#)f).x = r * f.x by A1,Def5; hence thesis by A2,RAT_1:def 2; end; end; registration let f be INT-valued Function, r be Integer; cluster r(#)f -> INT-valued; coherence proof let y be object; assume y in rng (r(#)f); then consider x being object such that A1: x in dom (r(#)f) and A2: (r(#)f).x = y by FUNCT_1:def 3; (r(#)f).x = r * f.x by A1,Def5; hence thesis by A2,INT_1:def 2; end; end; registration let f be natural-valued Function, r be Nat; cluster r(#)f -> natural-valued; coherence proof let x be object; assume x in dom (r(#)f); then (r(#)f).x = r * f.x by Def5; hence thesis; end; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; let r be Complex; redefine func r(#)f -> PartFunc of C,COMPLEX; coherence proof dom (r(#)f) = dom f & rng (r(#)f) c= COMPLEX by Def5,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; let r be Real; redefine func r(#)f -> PartFunc of C,REAL; coherence proof dom (r(#)f) = dom f & rng (r(#)f) c= REAL by Def5,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; let r be Rational; redefine func r(#)f -> PartFunc of C,RAT; coherence proof dom (r(#)f) = dom f & rng (r(#)f) c= RAT by Def5,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; let r be Integer; redefine func r(#)f -> PartFunc of C,INT; coherence proof dom (r(#)f) = dom f & rng (r(#)f) c= INT by Def5,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be natural-membered set; let f be PartFunc of C,D; let r be Nat; redefine func r(#)f -> PartFunc of C,NAT; coherence proof dom (r(#)f) = dom f & rng (r(#)f) c= NAT by Def5,VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; let r be Complex; cluster r(#)f -> total for PartFunc of C,COMPLEX; coherence proof dom(r(#)f) = dom f by Def5 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; let r be Real; cluster r(#)f -> total for PartFunc of C,REAL; coherence proof dom(r(#)f) = dom f by Def5 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; let r be Rational; cluster r(#)f -> total for PartFunc of C,RAT; coherence proof dom(r(#)f) = dom f by Def5 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; let r be Integer; cluster r(#)f -> total for PartFunc of C,INT; coherence proof dom(r(#)f) = dom f by Def5 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be natural-membered non empty set; let f be Function of C,D; let r be Nat; cluster r(#)f -> total for PartFunc of C,NAT; coherence proof dom(r(#)f) = dom f by Def5 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; theorem for C being non empty set, D being complex-membered non empty set for f being Function of C,D, r being Complex for g being Function of C, COMPLEX st for c being Element of C holds g.c = r * f.c holds g = r(#)f proof let C be non empty set, D be complex-membered non empty set; let f be Function of C,D, r be Complex; let g be Function of C,COMPLEX such that A1: for c being Element of C holds g.c = r * f.c; let x be Element of C; thus g.x = r*f.x by A1 .= (r(#)f).x by Th6; end; registration let f be complex-valued FinSequence, r be Complex; cluster r(#)f -> FinSequence-like; coherence proof dom (r(#)f) = dom f by Def5; hence thesis by Lm1; end; end; begin :: -f definition let f be complex-valued Function; func -f -> complex-valued Function equals (-1) (#) f; coherence; involutiveness proof let r, h be complex-valued Function; assume A1: r = (-1)(#)h; thus dom ((-1)(#)r) = dom r by Def5 .= dom h by A1,Def5; let c be object; assume c in dom h; reconsider a = (-1)*(h.c) as Complex; thus h.c = (-1) * a .= (-1)*r.c by A1,Th6 .= ((-1)(#)r).c by Th6; end; end; theorem Th8: for f being complex-valued Function holds dom -f = dom f & for c being object holds (-f).c = -(f.c) proof let f be complex-valued Function; thus A1: dom -f = dom f by Def5; let c be object; per cases; suppose c in dom f; hence (-f).c = (-1)*f.c by A1,Def5 .= -(f.c); end; suppose A2: not c in dom f; hence (-f).c = -(0 qua Complex) by A1,FUNCT_1:def 2 .= -(f.c) by A2,FUNCT_1:def 2; end; end; theorem for f being complex-valued Function, g being Function st dom f = dom g & for c being object st c in dom f holds g.c = -(f.c) holds g = -f proof let f be complex-valued Function, g be Function; assume that A1: dom f = dom g and A2: for c being object st c in dom f holds g.c = -(f.c); thus dom -f = dom g by A1,Def5; let c be object; assume A3: c in dom g; thus (-f).c = -f.c by Th8 .= g.c by A1,A2,A3; end; registration let f be complex-valued Function; cluster -f -> complex-valued; coherence; end; registration let f be real-valued Function; cluster -f -> real-valued; coherence; end; registration let f be RAT-valued Function; cluster -f -> RAT-valued; coherence; end; registration let f be INT-valued Function; cluster -f -> INT-valued; coherence; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; redefine func -f -> PartFunc of C,COMPLEX; coherence proof dom -f = dom f & rng -f c= COMPLEX by Def5,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; redefine func -f -> PartFunc of C,REAL; coherence proof dom -f = dom f & rng -f c= REAL by Def5,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; redefine func -f -> PartFunc of C,RAT; coherence proof dom -f = dom f & rng -f c= RAT by Def5,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; redefine func -f -> PartFunc of C,INT; coherence proof dom -f = dom f & rng -f c= INT by Def5,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; cluster -f -> total for PartFunc of C,COMPLEX; coherence; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; cluster -f -> total for PartFunc of C,REAL; coherence; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; cluster -f -> total for PartFunc of C,RAT; coherence; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; cluster -f -> total for PartFunc of C,INT; coherence; end; registration let f be complex-valued FinSequence; cluster -f -> FinSequence-like; coherence; end; begin :: f" definition let f be complex-valued Function; deffunc F(object) = (f.$1)"; func f" -> complex-valued Function means :Def7: dom it = dom f & for c being object st c in dom it holds it.c = (f.c)"; existence proof consider g being Function such that A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; g is complex-valued proof let x be object; assume x in dom g; then g.x = (f.x)" by A1; hence thesis; end; hence thesis by A1; end; uniqueness proof let h, g be complex-valued Function such that A2: dom h = dom f and A3: for c being object st c in dom h holds h.c = F(c) and A4: dom g = dom f and A5: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A6: x in dom h; hence h.x = F(x) by A3 .= g.x by A2,A4,A5,A6; end; hence thesis by A2,A4; end; involutiveness proof let r, h be complex-valued Function; assume that A7: dom r = dom h and A8: for c being object st c in dom r holds r.c = (h.c)"; thus dom r = dom h by A7; let c be object; assume A9: c in dom h; thus h.c = (h.c)"" .= (r.c)" by A7,A8,A9; end; end; ::better name theorem Th10: for f being complex-valued Function for c being object holds f".c = (f.c)" proof let f be complex-valued Function; let c be object; A1: dom (f") = dom f by Def7; per cases; suppose c in dom f; hence thesis by A1,Def7; end; suppose A2: not c in dom f; hence f".c = 0 qua Complex" by A1,FUNCT_1:def 2 .= (f.c)" by A2,FUNCT_1:def 2; end; end; registration let f be real-valued Function; cluster f" -> real-valued; coherence proof let x be object; assume x in dom (f"); then f".x = (f.x)" by Def7; hence thesis; end; end; registration let f be RAT-valued Function; cluster f" -> RAT-valued; coherence proof let y be object; assume y in rng (f"); then consider x being object such that A1: x in dom (f") and A2: (f").x = y by FUNCT_1:def 3; f".x = (f.x)" by A1,Def7; hence thesis by A2,RAT_1:def 2; end; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; redefine func f" -> PartFunc of C,COMPLEX; coherence proof dom (f") = dom f & rng (f") c= COMPLEX by Def7,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; redefine func f" -> PartFunc of C,REAL; coherence proof dom (f") = dom f & rng (f") c= REAL by Def7,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; redefine func f" -> PartFunc of C,RAT; coherence proof dom (f") = dom f & rng (f") c= RAT by Def7,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; cluster f" -> total for PartFunc of C,COMPLEX; coherence proof dom (f") = dom f by Def7 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; cluster f" -> total for PartFunc of C,REAL; coherence proof dom (f") = dom f by Def7 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; cluster f" -> total for PartFunc of C,RAT; coherence proof dom (f") = dom f by Def7 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let f be complex-valued FinSequence; cluster f" -> FinSequence-like; coherence proof dom (f") = dom f by Def7; hence thesis by Lm1; end; end; begin :: f^2 definition let f be complex-valued Function; func f^2 -> Function equals f (#) f; coherence; end; theorem Th11: for f being complex-valued Function holds dom (f^2) = dom f & for c being object holds f^2.c = (f.c)^2 proof let f be complex-valued Function; thus A1: dom (f^2) = dom f /\ dom f by Def4 .= dom f; let c be object; per cases; suppose c in dom f; hence thesis by A1,Def4; end; suppose A2: not c in dom f; hence f^2.c = 0 qua Complex^2 by A1,FUNCT_1:def 2 .= (f.c)^2 by A2,FUNCT_1:def 2; end; end; registration let f be complex-valued Function; cluster f^2 -> complex-valued; coherence; end; registration let f be real-valued Function; cluster f^2 -> real-valued; coherence; end; registration let f be RAT-valued Function; cluster f^2 -> RAT-valued; coherence; end; registration let f be INT-valued Function; cluster f^2 -> INT-valued; coherence; end; registration let f be natural-valued Function; cluster f^2 -> natural-valued; coherence; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; redefine func f^2 -> PartFunc of C,COMPLEX; coherence proof dom (f^2) = dom f & rng (f^2) c= COMPLEX by Th11,VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; redefine func f^2 -> PartFunc of C,REAL; coherence proof dom (f^2) = dom f & rng (f^2) c= REAL by Th11,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; redefine func f^2 -> PartFunc of C,RAT; coherence proof dom (f^2) = dom f & rng (f^2) c= RAT by Th11,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; redefine func f^2 -> PartFunc of C,INT; coherence proof dom (f^2) = dom f & rng (f^2) c= INT by Th11,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be natural-membered set; let f be PartFunc of C,D; redefine func f^2 -> PartFunc of C,NAT; coherence proof dom (f^2) = dom f & rng (f^2) c= NAT by Th11,VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; cluster f^2 -> total for PartFunc of C,COMPLEX; coherence; end; registration let C be set; let D be real-membered non empty set; let f be Function of C,D; cluster f^2 -> total for PartFunc of C,REAL; coherence; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; cluster f^2 -> total for PartFunc of C,RAT; coherence; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; cluster f^2 -> total for PartFunc of C,INT; coherence; end; registration let C be set; let D be natural-membered non empty set; let f be Function of C,D; cluster f^2 -> total for PartFunc of C,NAT; coherence; end; registration let f be complex-valued FinSequence; cluster f^2 -> FinSequence-like; coherence; end; begin :: f1 - f2 definition let f1,f2 be complex-valued Function; func f1 - f2 -> Function equals f1 + - f2; coherence; end; registration let f1,f2 be complex-valued Function; cluster f1-f2 -> complex-valued; coherence; end; registration let f1,f2 be real-valued Function; cluster f1-f2 -> real-valued; coherence; end; registration let f1,f2 be RAT-valued Function; cluster f1-f2 -> RAT-valued; coherence; end; registration let f1,f2 be INT-valued Function; cluster f1-f2 -> INT-valued; coherence; end; theorem Th12: for f1,f2 being complex-valued Function holds dom (f1-f2) = dom f1 /\ dom f2 proof let f1,f2 be complex-valued Function; thus dom (f1-f2) = dom f1 /\ dom -f2 by Def1 .= dom f1 /\ dom f2 by Def5; end; theorem for f1,f2 being complex-valued Function for c being object st c in dom (f1-f2) holds (f1-f2).c = f1.c - f2.c proof let f1,f2 be complex-valued Function; let c be object; assume c in dom (f1-f2); hence (f1-f2).c = f1.c+(-f2).c by Def1 .= f1.c-f2.c by Th8; end; theorem for f1,f2 being complex-valued Function, f being Function st dom f = dom (f1-f2) & for c being object st c in dom f holds f.c = f1.c - f2.c holds f = f1-f2 proof let f1,f2 be complex-valued Function, f be Function such that A1: dom f = dom (f1-f2) and A2: for c being object st c in dom f holds f.c = f1.c - f2.c; thus dom f = dom (f1-f2) by A1; let c be object; assume A3: c in dom f; hence f.c = f1.c - f2.c by A2 .= f1.c+(-f2).c by Th8 .= (f1-f2).c by A1,A3,Def1; end; definition let C be set; let D1,D2 be complex-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1-f2 -> PartFunc of C,COMPLEX; coherence proof dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= COMPLEX by Th12, VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be real-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1-f2 -> PartFunc of C,REAL; coherence proof dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= REAL by Th12,VALUED_0:def 3 ; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be rational-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1-f2 -> PartFunc of C,RAT; coherence proof dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= RAT by Th12,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be integer-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1-f2 -> PartFunc of C,INT; coherence proof dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= INT by Th12,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; Lm3: for C being set, D1,D2 being complex-membered non empty set, f1 being Function of C,D1, f2 being Function of C,D2 holds dom(f1-f2) = C proof let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; thus dom(f1-f2) = dom f1 /\ dom -f2 by Def1 .= C /\ dom -f2 by FUNCT_2:def 1 .= C /\ C by FUNCT_2:def 1 .= C; end; registration let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1-f2 -> total for PartFunc of C,COMPLEX; coherence by Lm3,PARTFUN1:def 2; end; registration let C be set; let D1,D2 be real-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1-f2 -> total for PartFunc of C,REAL; coherence by Lm3,PARTFUN1:def 2; end; registration let C be set; let D1,D2 be rational-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1-f2 -> total for PartFunc of C,RAT; coherence by Lm3,PARTFUN1:def 2; end; registration let C be set; let D1,D2 be integer-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1-f2 -> total for PartFunc of C,INT; coherence by Lm3,PARTFUN1:def 2; end; theorem for C being set, D1,D2 being complex-membered non empty set for f1 being Function of C,D1, f2 being Function of C,D2 for c being Element of C holds (f1-f2).c = f1.c - f2.c proof let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1, f2 be Function of C,D2; let c be Element of C; A1: dom(f1-f2) = C by FUNCT_2:def 1; per cases; suppose C is non empty; hence (f1-f2).c = f1.c + (-f2).c by A1,Def1 .= f1.c - f2.c by Th8; end; suppose A2: C is empty; then f2.c = 0; hence thesis by A2; end; end; registration let f1, f2 be complex-valued FinSequence; cluster f1-f2 -> FinSequence-like; coherence; end; begin :: f1 /" f2 definition let f1,f2 be complex-valued Function; func f1 /" f2 -> Function equals f1 (#) (f2"); coherence; end; theorem Th16: for f1,f2 being complex-valued Function holds dom (f1/"f2) = dom f1 /\ dom f2 proof let f1,f2 be complex-valued Function; thus dom (f1/"f2) = dom f1 /\ dom (f2") by Def4 .= dom f1 /\ dom f2 by Def7; end; theorem for f1,f2 being complex-valued Function for c being object holds (f1/"f2).c = f1.c / f2.c proof let f1,f2 be complex-valued Function; let c be object; A1: dom (f1/"f2) = dom f1 /\ dom f2 by Th16; per cases; suppose c in dom (f1/"f2); hence (f1/"f2).c = f1.c * (f2").c by Def4 .= f1.c / f2.c by Th10; end; suppose A2: not c in dom (f1/"f2); then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4; then A3: f1.c = 0 or f2.c = 0 by FUNCT_1:def 2; thus (f1/"f2).c = 0 / 0 by A2,FUNCT_1:def 2 .= f1.c / f2.c by A3; end; end; registration let f1,f2 be complex-valued Function; cluster f1/"f2 -> complex-valued; coherence; end; registration let f1,f2 be real-valued Function; cluster f1/"f2 -> real-valued; coherence; end; registration let f1,f2 be RAT-valued Function; cluster f1/"f2 -> RAT-valued; coherence; end; definition let C be set; let D1,D2 be complex-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1/"f2 -> PartFunc of C,COMPLEX; coherence proof dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= COMPLEX by Th16, VALUED_0:def 1; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be real-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1/"f2 -> PartFunc of C,REAL; coherence proof dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= REAL by Th16, VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D1,D2 be rational-membered set; let f1 be PartFunc of C,D1; let f2 be PartFunc of C,D2; redefine func f1/"f2 -> PartFunc of C,RAT; coherence proof dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= RAT by Th16, RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; Lm4: for C being set, D1,D2 being complex-membered non empty set for f1 being Function of C,D1, f2 being Function of C,D2 holds dom(f1/"f2) = C proof let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1, f2 be Function of C,D2; thus dom(f1/"f2) = dom f1 /\ dom f2 by Th16 .= C /\ dom f2 by FUNCT_2:def 1 .= C /\ C by FUNCT_2:def 1 .= C; end; registration let C be set; let D1,D2 be complex-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1/"f2 -> total for PartFunc of C,COMPLEX; coherence by Lm4,PARTFUN1:def 2; end; registration let C be set; let D1,D2 be real-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1/"f2 -> total for PartFunc of C,REAL; coherence by Lm4,PARTFUN1:def 2; end; registration let C be set; let D1,D2 be rational-membered non empty set; let f1 be Function of C,D1; let f2 be Function of C,D2; cluster f1/"f2 -> total for PartFunc of C,RAT; coherence by Lm4,PARTFUN1:def 2; end; registration let f1, f2 be complex-valued FinSequence; cluster f1/"f2 -> FinSequence-like; coherence; end; begin :: abs f definition let f be complex-valued Function; deffunc F(object) = |.f.$1.|; func |. f .| -> real-valued Function means :Def11: dom it = dom f & for c being object st c in dom it holds it.c = |. f.c .|; existence proof consider g being Function such that A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; g is real-valued proof let x be object; assume x in dom g; then g.x = |. f.x .| by A1; hence thesis; end; hence thesis by A1; end; uniqueness proof let h, g be real-valued Function such that A2: dom h = dom f and A3: for c being object st c in dom h holds h.c = F(c) and A4: dom g = dom f and A5: for c being object st c in dom g holds g.c = F(c); now let x be object; assume A6: x in dom h; hence h.x = F(x) by A3 .= g.x by A2,A4,A5,A6; end; hence thesis by A2,A4; end; projectivity proof let r be real-valued Function; let h be complex-valued Function; assume that dom r = dom h and A7: for c being object st c in dom r holds r.c = |.h.c.|; thus dom r = dom r; let c be object; assume A8: c in dom r; hence r.c = |.|.h.c.|.| by A7 .= |.r.c.| by A7,A8; end; end; notation let f be complex-valued Function; synonym abs f for |. f .|; end; theorem for f being complex-valued Function for c being object holds |.f.|.c = |.f.c.| proof let f be complex-valued Function; let c be object; A1: dom |.f.| = dom f by Def11; per cases; suppose c in dom f; hence thesis by A1,Def11; end; suppose A2: not c in dom f; hence |.f.|.c = |.0 qua Complex.| by A1,COMPLEX1:44,FUNCT_1:def 2 .= |.f.c.| by A2,FUNCT_1:def 2; end; end; registration let f be RAT-valued Function; cluster |.f.| -> RAT-valued; coherence proof let y be object; assume y in rng |.f.|; then consider x being object such that A1: x in dom |.f.| and A2: (|.f.|).x = y by FUNCT_1:def 3; |.f.|.x = |.f.x.| by A1,Def11; hence thesis by A2,RAT_1:def 2; end; end; registration let f be INT-valued Function; cluster |.f.| -> natural-valued; coherence proof let x be object; |.f.x.| is natural; hence thesis by Def11; end; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; redefine func |.f.| -> PartFunc of C,REAL; coherence proof dom |.f.| = dom f & rng |.f.| c= REAL by Def11,VALUED_0:def 3; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be complex-membered set; let f be PartFunc of C,D; redefine func abs(f) -> PartFunc of C,REAL; coherence proof abs(f) = |.f.|; hence thesis; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; redefine func |.f.| -> PartFunc of C,RAT; coherence proof dom |.f.| = dom f & rng |.f.| c= RAT by Def11,RELAT_1:def 19; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be rational-membered set; let f be PartFunc of C,D; redefine func abs(f) -> PartFunc of C,RAT; coherence proof abs(f) = |.f.|; hence thesis; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; redefine func |.f.| -> PartFunc of C,NAT; coherence proof dom |.f.| = dom f & rng |.f.| c= NAT by Def11,VALUED_0:def 6; hence thesis by RELSET_1:4; end; end; definition let C be set; let D be integer-membered set; let f be PartFunc of C,D; redefine func abs(f) -> PartFunc of C,NAT; coherence proof abs(f) = |.f.|; hence thesis; end; end; registration let C be set; let D be complex-membered non empty set; let f be Function of C,D; cluster |.f.| -> total for PartFunc of C,REAL; coherence proof dom |.f.| = dom f by Def11 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be rational-membered non empty set; let f be Function of C,D; cluster |.f.| -> total for PartFunc of C,RAT; coherence proof dom |.f.| = dom f by Def11 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let C be set; let D be integer-membered non empty set; let f be Function of C,D; cluster |.f.| -> total for PartFunc of C,NAT; coherence proof dom |.f.| = dom f by Def11 .= C by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration let f be complex-valued FinSequence; cluster |.f.| -> FinSequence-like; coherence proof dom abs f = dom f by Def11; hence thesis by Lm1; end; end; theorem for f, g being FinSequence, h being Function st dom h = dom f /\ dom g holds h is FinSequence by Lm2; begin :: Addenda :: from RELOC, 2008.02.14, A.T. reserve m,j,p,q,n,l for Element of NAT; definition let p be Function, k be Nat; func Shift(p,k) -> Function means :Def12: dom it = { m+k where m is Nat:m in dom p } & for m being Nat st m in dom p holds it.(m+k) = p.m; existence proof defpred P[object,object] means ex m being Nat st $1 = m+k & $2 = p.m; set A = { m+k where m is Nat:m in dom p }; A1: for e being object st e in A ex u being object st P[e,u] proof let e be object; assume e in A; then consider m being Nat such that A2: e = m+k and m in dom p; take p.m; thus thesis by A2; end; consider f being Function such that A3: dom f = A and A4: for e being object st e in A holds P[e,f.e] from CLASSES1:sch 1(A1); take f; thus dom f = { m+k where m is Nat :m in dom p } by A3; let m be Nat; assume m in dom p; then m+k in A; then ex j being Nat st m+k = j+k & f.(m+k) = p.j by A4; hence thesis; end; uniqueness proof let IT1,IT2 be Function such that A5: dom IT1 = { m+k where m is Nat:m in dom p } and A6: for m being Nat st m in dom p holds IT1.(m+k) = p.m and A7: dom IT2 = { m+k where m is Nat:m in dom p } and A8: for m being Nat st m in dom p holds IT2.(m+k) = p.m; for x being object st x in dom IT1 holds IT1.x = IT2.x proof let x be object; assume x in dom IT1; then consider m being Nat such that A9: x = m+k & m in dom p by A5; thus IT1.x = p.m by A6,A9 .= IT2.x by A8,A9; end; hence thesis by A5,A7; end; end; registration let p be Function, k be Nat; cluster Shift(p,k) -> NAT-defined; coherence proof A1: dom Shift(p,k) = { m+k where m is Nat:m in dom p } by Def12; Shift(p,k) is NAT-defined proof let x be object; assume x in dom Shift(p,k); then ex m being Nat st x = m+k & m in dom p by A1; hence thesis by ORDINAL1:def 12; end; hence thesis; end; end; theorem :: SCMFSA8C:11 for P,Q being Function, k being Nat st P c= Q holds Shift(P ,k) c= Shift(Q,k) proof let P,Q be Function; let k be Nat; assume A1: P c= Q; then A2: dom P c= dom Q by GRFUNC_1:2; A3: dom Shift(P,k) = {m + k where m is Nat: m in dom P} by Def12; A4: dom Shift(Q,k) = {m + k where m is Nat: m in dom Q} by Def12; A5: now let x be object; assume x in dom Shift(P,k); then ex m1 being Nat st x = m1 + k & m1 in dom P by A3; hence x in dom Shift(Q,k) by A2,A4; end; now let x be object; assume x in dom Shift(P,k); then consider m1 being Nat such that A6: x = m1 + k and A7: m1 in dom P by A3; thus Shift(P,k).x = Shift(P,k).(m1 + k) by A6 .= P.m1 by A7,Def12 .= Q.m1 by A1,A7,GRFUNC_1:2 .= Shift(Q,k).(m1 + k) by A2,A7,Def12 .= Shift(Q,k).x by A6; end; hence thesis by A5,GRFUNC_1:2,TARSKI:def 3; end; theorem :: SCMFSA_4:32 for n,m being Nat for I being Function holds Shift(Shift(I,m),n) = Shift(I,m+n) proof let n,m be Nat; let I be Function; set A = {l+m where l is Nat:l in dom I }; A1: dom Shift(I,m) = A by Def12; A2: now let l be Nat; assume A3: l in dom I; then A4: l+m in dom Shift(I,m) by A1; thus Shift(Shift(I,m),n).(l+(m+n)) = Shift(Shift(I,m),n).(l+m+n) .= Shift(I,m).(l+m) by A4,Def12 .= I.l by A3,Def12; end; {p+n where p is Nat: p in A } = { q+(m+n) where q is Nat: q in dom I} proof thus {p+n where p is Nat: p in A } c= { q+(m+n) where q is Nat: q in dom I} proof let x be object; assume x in {p+n where p is Nat: p in A }; then consider p being Nat such that A5: x = p+n and A6: p in A; consider l being Nat such that A7: p = l+m and A8: l in dom I by A6; x = l+(m+n) by A5,A7; hence thesis by A8; end; let x be object; assume x in { q+(m+n) where q is Nat: q in dom I}; then consider q being Nat such that A9: x = q+(m+n) & q in dom I; x = (q+m)+n & q+m in A by A9; hence thesis; end; then dom Shift(Shift(I,m),n) = { l+(m+n) where l is Nat: l in dom I} by A1,Def12; hence thesis by A2,Def12; end; theorem :: SCMFSA_4:33 for s,f be Function for n being Nat holds Shift(f*s,n) = f*Shift(s,n) proof let s,f be Function; let n be Nat; A1: dom(f*s) c= dom s by RELAT_1:25; A2: dom Shift(s,n)= { m+n where m is Nat: m in dom s } by Def12; now let e be object; thus e in { m+n where m is Nat: m in dom(f*s) } implies e in dom Shift(s,n) & Shift(s,n). e in dom f proof assume e in { m+n where m is Nat: m in dom(f*s) }; then consider m being Nat such that A3: e = m+n and A4: m in dom(f*s); thus e in dom Shift(s,n) by A2,A1,A3,A4; Shift(s,n).e = s.m by A1,A3,A4,Def12; hence thesis by A4,FUNCT_1:11; end; assume e in dom Shift(s,n); then consider m0 being Nat such that A5: e = m0+n and A6: m0 in dom s by A2; assume Shift(s,n).e in dom f; then s.m0 in dom f by A5,A6,Def12; then m0 in dom(f*s) by A6,FUNCT_1:11; hence e in { m+n where m is Nat: m in dom(f*s) } by A5; end; then Shift(s,n)"dom f = { m+n where m is Nat: m in dom(f*s) } by FUNCT_1:def 7; then A7: dom(f*Shift(s,n)) = { m+n where m is Nat: m in dom(f*s) } by RELAT_1:147; now let m be Nat; assume A8: m in dom(f*s); then m+n in dom Shift(s,n) by A2,A1; hence (f*Shift(s,n)).(m+n) = f.(Shift(s,n).(m+n)) by FUNCT_1:13 .= f.(s.m) by A1,A8,Def12 .= (f*s).m by A8,FUNCT_1:12; end; hence thesis by A7,Def12; end; theorem :: SCMFSA_4:34 for I,J being Function, n being Nat holds Shift(I +* J, n) = Shift(I,n) +* Shift(J,n) proof let I,J be Function, n be Nat; A1: dom Shift(J,n) = { m+n where m is Nat: m in dom J } by Def12; A2: now let m be Nat such that A3: m in dom(I +* J); per cases; suppose A4: m in dom J; then m+n in dom Shift(J,n) by A1; hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(J,n).(m+n) by FUNCT_4:13 .= J.m by A4,Def12 .= (I +* J).m by A4,FUNCT_4:13; end; suppose A5: not m in dom J; m in dom I \/ dom J by A3,FUNCT_4:def 1; then A6: m in dom I by A5,XBOOLE_0:def 3; not ex l being Nat st m+n = l+n & l in dom J by A5; then not m+n in dom Shift(J,n) by A1; hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(I,n).(m+n) by FUNCT_4:11 .= I.m by A6,Def12 .= (I +* J).m by A5,FUNCT_4:11; end; end; A7: dom Shift(I,n) = { m+n where m is Nat: m in dom I } by Def12; A8: dom Shift(I,n) \/ dom Shift(J,n) = { m+n where m is Nat: m in dom I \/ dom J } proof hereby let x be object; assume x in dom Shift(I,n) \/ dom Shift(J,n); then x in dom Shift(I,n) or x in dom Shift(J,n) by XBOOLE_0:def 3; then consider m being Nat such that A9: x = m+n & m in dom J or x = m+n & m in dom I by A1,A7; m in dom I \/ dom J by A9,XBOOLE_0:def 3; hence x in { l+n where l is Nat: l in dom I \/ dom J } by A9; end; let x be object; assume x in { m+n where m is Nat: m in dom I \/ dom J }; then consider m being Nat such that A10: x = m+n and A11: m in dom I \/ dom J; m in dom I or m in dom J by A11,XBOOLE_0:def 3; then x in dom Shift(I,n) or x in dom Shift(J,n) by A1,A7,A10; hence thesis by XBOOLE_0:def 3; end; dom(I +* J) = dom I \/ dom J by FUNCT_4:def 1; then dom(Shift(I,n) +* Shift(J,n)) = { m+n where m is Nat: m in dom(I +* J ) } by A8,FUNCT_4:def 1; hence thesis by A2,Def12; end; :: from SCMPDS_4, 2008.03.16, A.T. theorem Th24: for p being Function,k,il being Nat st il in dom p holds il+k in dom Shift(p,k) proof let p be Function, k,il be Nat such that A1: il in dom p; dom Shift(p,k) = { loc+k where loc is Nat : loc in dom p} by Def12; hence thesis by A1; end; :: missing, 2008.03.16, A.T. theorem Th25: for p being Function, k being Nat holds rng Shift(p,k) c= rng p proof let p be Function, k being Nat; let y be object; assume y in rng Shift(p,k); then consider x being object such that A1: x in dom Shift(p,k) and A2: y = Shift(p,k).x by FUNCT_1:def 3; x in { m+k where m is Nat:m in dom p } by A1,Def12; then consider m being Nat such that A3: x = m+k and A4: m in dom p; p.m = Shift(p,k).x by A3,A4,Def12; hence thesis by A2,A4,FUNCT_1:def 3; end; theorem for p being Function st dom p c= NAT for k being Nat holds rng Shift(p,k) = rng p proof let p be Function such that A1: dom p c= NAT; let k be Nat; thus rng Shift(p,k) c= rng p by Th25; let y be object; assume y in rng p; then consider x being object such that A2: x in dom p and A3: y = p.x by FUNCT_1:def 3; reconsider x as Element of NAT by A1,A2; x+k in dom Shift(p,k) & Shift(p,k).(x+k) = y by A2,A3,Def12,Th24; hence thesis by FUNCT_1:def 3; end; registration let p be finite Function, k be Nat; cluster Shift(p,k) -> finite; coherence proof deffunc F(Nat) = $1+k; A1: dom p is finite; A2: { F(w) where w is Element of NAT: w in dom p } is finite from FRAENKEL:sch 21(A1); dom Shift(p,k) c= { F(w) where w is Element of NAT: w in dom p } proof let e be object; assume e in dom Shift(p,k); then e in { F(i) where i is Nat: i in dom p } by Def12; then consider i being Nat such that A3: e = F(i) & i in dom p; reconsider i as Element of NAT by ORDINAL1:def 12; e = F(i) & i in dom p by A3; hence e in { F(w) where w is Element of NAT: w in dom p }; end; hence thesis by A2,FINSET_1:10; end; end; reserve e1,e2 for ExtReal; definition let X be non empty ext-real-membered set, s be sequence of X; redefine attr s is increasing means for n being Nat holds s.n < s.(n+1); compatibility proof thus s is increasing implies for n being Nat holds s.n < s.(n+1 ) proof assume A1: s is increasing; let n be Nat; A2: n < n+1 by NAT_1:13; dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12; hence thesis by A1,A2; end; assume A3: for n being Nat holds s.n < s.(n+1); let e1,e2; assume e1 in dom s & e2 in dom s; then reconsider m=e1, n=e2 as Nat; defpred P[Nat] means m < $1 implies s.m < s.$1; A4: for j being Nat st P[j] holds P[j+1] proof let j being Nat such that A5: P[j]; assume m < j+1; then m <= j by NAT_1:13; then s.m < s.j or m = j by A5,XXREAL_0:1; hence thesis by A3,XXREAL_0:2; end; assume A6: e1 < e2; A7: P[0]; for j being Nat holds P[j] from NAT_1:sch 2(A7,A4); then s.m < s.n by A6; hence thesis; end; redefine attr s is decreasing means for n being Nat holds s.n > s.(n+1); compatibility proof thus s is decreasing implies for n being Nat holds s.n > s.(n+1 ) proof assume A8: s is decreasing; let n be Nat; A9: n < n+1 by NAT_1:13; dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12; hence thesis by A8,A9; end; assume A10: for n being Nat holds s.n > s.(n+1); let e1,e2; assume e1 in dom s & e2 in dom s; then reconsider m=e1, n=e2 as Nat; defpred P[Nat] means m < $1 implies s.m > s.$1; A11: for j being Nat st P[j] holds P[j+1] proof let j being Nat such that A12: P[j]; assume m < j+1; then m <= j by NAT_1:13; then s.m > s.j or m = j by A12,XXREAL_0:1; hence thesis by A10,XXREAL_0:2; end; assume A13: e1 < e2; A14: P[0]; for j being Nat holds P[j] from NAT_1:sch 2(A14,A11); then s.m > s.n by A13; hence thesis; end; redefine attr s is non-decreasing means for n being Nat holds s.n <= s.(n+1); compatibility proof thus s is non-decreasing implies for n being Nat holds s.n <= s.(n+1 ) proof assume A15: s is non-decreasing; let n be Nat; A16: n < n+1 by NAT_1:13; dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12; hence thesis by A15,A16; end; assume A17: for n being Nat holds s.n <= s.(n+1); let e1,e2; assume e1 in dom s & e2 in dom s; then reconsider m=e1, n=e2 as Nat; defpred P[Nat] means m <= $1 implies s.m <= s.$1; A18: for j being Nat st P[j] holds P[j+1] proof let j being Nat such that A19: P[j]; assume m <= j+1; then A20: m < j+1 or m = j+1 by XXREAL_0:1; s.j <= s.(j+1) by A17; hence thesis by A19,A20,NAT_1:13,XXREAL_0:2; end; assume A21: e1 <= e2; A22: P[0]; for j being Nat holds P[j] from NAT_1:sch 2(A22,A18); then s.m <= s.n by A21; hence thesis; end; redefine attr s is non-increasing means for n being Nat holds s.n >= s.(n+1); compatibility proof thus s is non-increasing implies for n being Nat holds s.n >= s.(n+1 ) proof assume A23: s is non-increasing; let n be Nat; A24: n < n+1 by NAT_1:13; dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12; hence thesis by A23,A24; end; assume A25: for n being Nat holds s.n >= s.(n+1); let e1,e2; assume e1 in dom s & e2 in dom s; then reconsider m=e1, n=e2 as Nat; defpred P[Nat] means m <= $1 implies s.m >= s.$1; A26: for j being Nat st P[j] holds P[j+1] proof let j being Nat such that A27: P[j]; assume m <= j+1; then A28: m < j+1 or m = j+1 by XXREAL_0:1; s.j >= s.(j+1) by A25; hence thesis by A27,A28,NAT_1:13,XXREAL_0:2; end; assume A29: e1 <= e2; A30: P[0]; for j being Nat holds P[j] from NAT_1:sch 2(A30,A26); then s.m >= s.n by A29; hence thesis; end; end; :: from KURATO_2, 2008.09.05, A.T. scheme SubSeqChoice { X() -> non empty set, S() -> sequence of X(), P[set]} : ex S1 being subsequence of S() st for n being Element of NAT holds P[S1.n] provided A1: for n being Element of NAT ex m being Element of NAT st n <= m & P[S ().m] proof defpred P1[set,set,set] means $3 in NAT & (for m,k being Element of NAT st m = $2 & k = $3 holds m < k & P[S().k]); consider n0 being Element of NAT such that 0 <= n0 and A2: P[S().n0] by A1; A3: for n being Nat for x being set ex y being set st P1[n,x,y] proof let n be Nat, x be set; per cases; suppose x in NAT; then reconsider mx = x as Element of NAT; consider my being Element of NAT such that A4: mx + 1 <= my & P[S().my] by A1; take my; thus my in NAT; thus thesis by A4,NAT_1:13; end; suppose A5: not x in NAT; take 0; set y = 0; thus y in NAT; let m, k be Element of NAT; assume that A6: m = x and k = y; thus thesis by A5,A6; end; end; consider g being Function such that A7: dom g = NAT and A8: g.0 = n0 and A9: for n being Nat holds P1[n,g.n,g.(n+1)] from RECDEF_1: sch 1(A3); rng g c= NAT proof defpred P[Nat] means g.$1 in NAT; let y be object; assume y in rng g; then consider x being object such that A10: x in dom g and A11: g.x = y by FUNCT_1:def 3; reconsider n = x as Element of NAT by A7,A10; A12: for k being Nat holds P[k] implies P[k+1] by A9; A13: P[0] by A8; for k being Nat holds P[k] from NAT_1:sch 2(A13,A12); then g.n in NAT; hence thesis by A11; end; then reconsider g as sequence of NAT by A7,FUNCT_2:2; g is increasing by A9; then reconsider g as increasing sequence of NAT; reconsider S1 = S() * g as sequence of X(); A14: dom S1 = NAT by FUNCT_2:def 1; reconsider S1 as subsequence of S(); take S1; thus for n being Element of NAT holds P[S1.n] proof let n be Element of NAT; per cases; suppose n = 0; hence thesis by A2,A8,A14,FUNCT_1:12; end; suppose n <> 0; then n >= 0 qua Nat + 1 by NAT_1:13; then reconsider n9 = n-1 as Element of NAT by INT_1:5; reconsider k = g.(n9+1) as Element of NAT; for m,k being Element of NAT st m = g.n9 & k = g.(n9+1) holds P[S() .k] by A9; then P[S().k]; hence thesis by A14,FUNCT_1:12; end; end; end; :: from AMISTD_2, 2010.02.05, A.T. theorem for k being Nat for F being NAT-defined Function holds dom F,dom Shift(F,k) are_equipotent proof let k be Nat; let F be NAT-defined Function; defpred P[object,object] means ex il being Element of NAT st $1 = il & $2 = k+il; A1: for e being object st e in dom F ex u being object st P[e,u] proof let e be object; assume e in dom F; then reconsider e as Element of NAT; take k+e, e; thus thesis; end; consider f being Function such that A2: dom f = dom F and A3: for x being object st x in dom F holds P[x,f.x] from CLASSES1:sch 1(A1); take f; hereby let x1, x2 be object such that A4: x1 in dom f and A5: x2 in dom f and A6: f.x1 = f.x2; consider i1 being Element of NAT such that A7: x1 = i1 and A8: f.x1 = k+i1 by A2,A3,A4; consider i2 being Element of NAT such that A9: x2 = i2 and A10: f.x2 = k+i2 by A2,A3,A5; thus x1 = x2 by A7,A6,A8,A10,A9; end; thus dom f = dom F by A2; A11: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12; hereby let y be object; assume y in rng f; then consider x being object such that A12: x in dom f and A13: f.x = y by FUNCT_1:def 3; consider il being Element of NAT such that A14: x = il and A15: f.x = k+il by A2,A3,A12; thus y in dom Shift(F,k) by A2,A11,A12,A13,A14,A15; end; let y be object; assume y in dom Shift(F,k); then consider m being Nat such that A16: y = (m+k) and A17: m in dom F by A11; consider il being Element of NAT such that A18: m = il and A19: f.m = k+il by A3,A17; thus thesis by A2,A16,A17,A18,A19,FUNCT_1:def 3; end; registration let F be NAT-defined Function; reduce Shift(F,0) to F; reducibility proof A1: dom F = { m+(0 qua Nat) where m is Nat: m in dom F } proof hereby let a be object; assume A2: a in dom F; then reconsider l=a as Element of NAT; a = (l qua Nat)+(0 qua Complex); hence a in { m+(0 qua Nat) where m is Nat: m in dom F } by A2; end; let a be object; assume a in { m+(0 qua Complex) where m is Nat: m in dom F }; then ex m being Nat st a = m+(0 qua Complex) & m in dom F; hence thesis; end; for m being Nat st m in dom F holds F.(m+(0 qua Complex)) = F.m; hence thesis by A1,Def12; end; end; registration let X be non empty set; let F be X-valued Function, k be Nat; cluster Shift(F,k) -> X-valued; coherence proof A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12; thus rng Shift(F,k) c= X proof let x be object; assume x in rng Shift(F,k); then consider y being object such that A2: y in dom Shift(F,k) and A3: x = Shift(F,k).y by FUNCT_1:def 3; consider m being Nat such that A4: y = (m+k) and A5: m in dom F by A2,A1; Shift(F,k).(m+k) = F.m by A5,Def12 .= F/.m by A5,PARTFUN1:def 6; hence x in X by A3,A4; end; end; end; registration :: move somewhere !!! cluster non empty NAT-defined for Function; existence proof take id NAT; thus thesis; end; end; registration let F be empty Function, k be Nat; cluster Shift(F,k) -> empty; coherence proof A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12; assume Shift(F,k) is non empty; then reconsider f = Shift(F,k) as non empty Function; dom f is non empty; then consider a being object such that A2: a in dom Shift(F,k); ex m being Nat st a = (m+k) & m in dom F by A1,A2; hence thesis; end; end; registration let F be non empty NAT-defined Function, k be Nat; cluster Shift(F,k) -> non empty; coherence proof A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12; consider a being object such that A2: a in dom F by XBOOLE_0:def 1; reconsider a as Element of NAT by A2; consider m being Nat such that A3: a = m; reconsider m as Element of NAT by ORDINAL1:def 12; (m+k) in dom Shift(F,k) by A1,A2,A3; hence thesis; end; end; ::$CT theorem for F being Function, k being Nat st k > 0 holds not 0 in dom Shift(F,k) proof let F be Function, k be Nat such that A1: k > 0 and A2: 0 in dom Shift(F,k); dom Shift(F,k) = { m+k where m is Nat: m in dom F } by Def12; then ex m being Nat st 0 = m+k & m in dom F by A2; hence contradiction by A1; end; registration cluster NAT-defined finite non empty for Function; existence proof take f = 0 .--> 0; dom f = {0} by FUNCOP_1:13; hence dom f c= NAT by ZFMISC_1:31; thus thesis; end; end; registration let F be NAT-defined Relation; cluster dom F -> natural-membered; coherence; end; definition let F be non empty NAT-defined finite Function; func LastLoc F -> Element of NAT equals max dom F; coherence by ORDINAL1:def 12; end; definition let F be non empty NAT-defined finite Function; func CutLastLoc F -> Function equals F \ ( LastLoc F .--> F.LastLoc F ); coherence; end; registration let F be non empty NAT-defined finite Function; cluster CutLastLoc F -> NAT-defined finite; coherence; end; theorem for F being non empty NAT-defined finite Function holds LastLoc F in dom F by XXREAL_2:def 8; theorem for F, G being non empty NAT-defined finite Function st F c= G holds LastLoc F <= LastLoc G by RELAT_1:11,XXREAL_2:59; theorem for F being non empty NAT-defined finite Function, l being Element of NAT st l in dom F holds l <= LastLoc F by XXREAL_2:def 8; definition let F be non empty NAT-defined Function; func FirstLoc F -> Element of NAT equals min dom F; coherence by ORDINAL1:def 12; end; theorem for F being non empty NAT-defined finite Function holds FirstLoc F in dom F by XXREAL_2:def 7; theorem for F, G being non empty NAT-defined finite Function st F c= G holds FirstLoc G <= FirstLoc F by RELAT_1:11,XXREAL_2:60; theorem for l1 being Element of NAT for F being non empty NAT-defined finite Function st l1 in dom F holds FirstLoc F <= l1 by XXREAL_2:def 7; theorem Th35: for F being non empty NAT-defined finite Function holds dom CutLastLoc F = (dom F) \ {LastLoc F} proof let F be non empty NAT-defined finite Function; A1: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F} by FUNCOP_1:13; reconsider R = {[LastLoc F, F.LastLoc F]} as Relation; A2: R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:82; then A3: dom R = {LastLoc F} by FUNCOP_1:13; thus dom CutLastLoc F c= (dom F) \ {LastLoc F} proof let x be object; assume x in dom CutLastLoc F; then consider y being object such that A4: [x,y] in F \ R by A2,XTUPLE_0:def 12; A5: not [x,y] in R by A4,XBOOLE_0:def 5; A6: x in dom F by A4,XTUPLE_0:def 12; per cases by A5,TARSKI:def 1; suppose x <> LastLoc F; then not x in dom R by A3,TARSKI:def 1; hence thesis by A1,A2,A6,XBOOLE_0:def 5; end; suppose A7: y <> F.LastLoc F; now assume x in dom R; then x = LastLoc F by A3,TARSKI:def 1; hence contradiction by A4,A7,FUNCT_1:1; end; hence thesis by A1,A2,A6,XBOOLE_0:def 5; end; end; thus thesis by A1,XTUPLE_0:25; end; theorem for F being non empty NAT-defined finite Function holds dom F = dom CutLastLoc F \/ {LastLoc F} proof let F be non empty NAT-defined finite Function; LastLoc F in dom F by XXREAL_2:def 8; then A1: {LastLoc F} c= dom F by ZFMISC_1:31; dom CutLastLoc F = (dom F) \ {LastLoc F} by Th35; hence thesis by A1,XBOOLE_1:45; end; registration cluster 1-element NAT-defined finite for Function; existence proof take 0 .--> 0; thus thesis; end; end; registration let F be 1-element NAT-defined finite Function; cluster CutLastLoc F -> empty; coherence proof LastLoc F in dom F by XXREAL_2:def 8; then A1: [LastLoc F,F.LastLoc F] in F by FUNCT_1:def 2; assume not thesis; then consider a being object such that A2: a in CutLastLoc F; A3: a = [LastLoc F,F.LastLoc F] by A1,A2,ZFMISC_1:def 10; not a in LastLoc F .--> F.LastLoc F by A2,XBOOLE_0:def 5; then not a in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82; hence thesis by A3,TARSKI:def 1; end; end; theorem Th37: for F being non empty NAT-defined finite Function holds card CutLastLoc F = card F - 1 proof let F be non empty NAT-defined finite Function; LastLoc F .--> F.LastLoc F c= F proof let a, b be object; assume [a,b] in LastLoc F .--> F.LastLoc F; then [a,b] in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82; then A1: [a,b] = [LastLoc F,F.LastLoc F] by TARSKI:def 1; LastLoc F in dom F by XXREAL_2:def 8; hence thesis by A1,FUNCT_1:def 2; end; hence card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F) by CARD_2:44 .= card F - card {[LastLoc F,F.LastLoc F]} by FUNCT_4:82 .= card F - 1 by CARD_1:30; end; begin :: 2011.04.20, A.T. registration let X be set, f be X-defined complex-valued Function; cluster -f -> X-defined; coherence proof A1: dom -f = dom f by Def5; thus dom -f c= X by A1; end; cluster f" -> X-defined; coherence proof A2: dom(f") = dom f by Def7; thus dom(f") c= X by A2; end; cluster f^2 -> X-defined; coherence proof A3: dom(f^2) = dom f by Th11; thus dom(f^2) c= X by A3; end; cluster |.f.| -> X-defined; coherence proof A4: dom |.f.| = dom f by Def11; thus dom |.f.| c= X by A4; end; end; registration let X be set; cluster total for X-defined natural-valued Function; existence proof take the total PartFunc of X, NAT; thus thesis; end; end; registration let X be set, f be total X-defined complex-valued Function; cluster -f -> total; coherence proof A1: dom -f = dom f by Def5; dom f = X by PARTFUN1:def 2; hence thesis by A1,PARTFUN1:def 2; end; cluster f" -> total; coherence proof A2: dom(f") = dom f by Def7; dom f = X by PARTFUN1:def 2; hence thesis by A2,PARTFUN1:def 2; end; cluster f^2 -> total; coherence proof A3: dom(f^2) = dom f by Th11; dom f = X by PARTFUN1:def 2; hence thesis by A3,PARTFUN1:def 2; end; cluster |.f.| -> total; coherence proof A4: dom |.f.| = dom f by Def11; dom f = X by PARTFUN1:def 2; hence thesis by A4,PARTFUN1:def 2; end; end; registration let X be set, f be X-defined complex-valued Function, r be Complex; cluster r+f -> X-defined; coherence proof A1: dom(r+f) = dom f by Def2; thus dom(r+f) c= X by A1; end; cluster f-r -> X-defined; coherence; cluster r(#)f -> X-defined; coherence proof A2: dom(r(#)f) = dom f by Def5; thus dom(r(#)f) c= X by A2; end; end; registration let X be set, f be total X-defined complex-valued Function, r be Complex; cluster r+f -> total; coherence proof A1: dom(r+f) = dom f by Def2; dom f = X by PARTFUN1:def 2; hence thesis by A1,PARTFUN1:def 2; end; cluster f-r -> total; coherence; cluster r(#)f -> total; coherence proof A2: dom(r(#)f) = dom f by Def5; dom f = X by PARTFUN1:def 2; hence thesis by A2,PARTFUN1:def 2; end; end; registration let X be set, f1 be complex-valued Function; let f2 be X-defined complex-valued Function; cluster f1 + f2 -> X-defined; coherence proof A1: dom(f1 + f2) = dom f1 /\ dom f2 by Def1; thus dom(f1 + f2) c= X by A1; end; cluster f1 - f2 -> X-defined; coherence; cluster f1(#)f2 -> X-defined; coherence proof A2: dom(f1(#)f2) = dom f1 /\ dom f2 by Def4; thus dom(f1(#)f2) c= X by A2; end; cluster f1/"f2 -> X-defined; coherence; end; registration let X be set; let f1,f2 be total X-defined complex-valued Function; cluster f1 + f2 -> total; coherence proof A1: dom(f1 + f2) = dom f1 /\ dom f2 by Def1; dom f1 = X & dom f2 = X by PARTFUN1:def 2; hence thesis by A1,PARTFUN1:def 2; end; cluster f1 - f2 -> total; coherence; cluster f1(#)f2 -> total; coherence proof A2: dom(f1(#)f2) = dom f1 /\ dom f2 by Def4; dom f1 = X & dom f2 = X by PARTFUN1:def 2; hence thesis by A2,PARTFUN1:def 2; end; cluster f1/"f2 -> total; coherence; end; registration let X be non empty set; let F be X-valued non empty NAT-defined finite Function; cluster CutLastLoc F -> X-valued; coherence; end; theorem for f being Function for i,n being Nat st i in dom Shift(f,n) ex j being Nat st j in dom f & i = j + n proof let f be Function; let i,n be Nat; A1: dom Shift(f,n) = { m+n where m is Nat:m in dom f } by Def12; assume i in dom Shift(f,n); then ex m being Nat st i = m + n & m in dom f by A1; hence ex j being Nat st j in dom f & i = j + n; end; :: from PNPROC_1, 2012.02.20, A.T. registration let p be FinSubsequence; let i be Nat; cluster Shift(p,i) -> FinSubsequence-like; coherence proof set X = {k+i where k is Nat : k in dom p }, f = Shift(p,i); consider K being Nat such that A1: dom p c= Seg K by FINSEQ_1:def 12; A2: dom f = X by Def12; X c= Seg (i+K) proof let x be object; assume x in X; then consider k being Nat such that A3: x = k+i and A4: k in dom p; A5: i+k >= k by NAT_1:11; A6: k >= 1 by A1,A4,FINSEQ_1:1; A7: k <= K by A1,A4,FINSEQ_1:1; i+k >= 1 by A5,A6,XXREAL_0:2; hence thesis by A3,A7,FINSEQ_1:1,XREAL_1:6; end; hence f is FinSubsequence-like by A2; end; end; reserve i for Nat, k,k1,k2,j1 for Element of NAT, x,x1,x2,y for set; theorem Th39: for p being FinSequence holds dom Shift(p,i) = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)} proof let p be FinSequence; A1: dom p = Seg len p by FINSEQ_1:def 3 .= {k where k is Nat: 1 <= k & k <= len p}; set X = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)}; A2: dom Shift(p,i) = {k1+i where k1 is Nat: k1 in dom p} by Def12; thus dom Shift(p,i) c= X proof let x be object; assume x in dom Shift(p,i); then consider k1 being Nat such that A3: x = k1+i and A4: k1 in dom p by A2; consider k being Nat such that A5: k1 = k and A6: 1 <= k and A7: k <= len p by A1,A4; A8: i+1 <= i+k by A6,XREAL_1:7; i+k <= i+(len p) by A7,XREAL_1:7; hence thesis by A3,A5,A8; end; let x be object; assume x in X; then consider j1 being Nat such that A9: x = j1 and A10: i+1 <= j1 and A11: j1 <= i+(len p); i+(0 qua Nat) <= i+1 by XREAL_1:7; then consider k2 being Nat such that A12: j1 = i+k2 by A10,NAT_1:10,XXREAL_0:2; A13: 1 <= k2 by A10,A12,XREAL_1:6; k2 <= len p by A11,A12,XREAL_1:6; then k2 in dom p by A1,A13; hence thesis by A2,A9,A12; end; theorem Th40: for q being FinSubsequence ex ss being FinSubsequence st dom ss = dom q & rng ss = dom Shift(q,i) & (for k st k in dom q holds ss.k = i+k) & ss is one-to-one proof let q be FinSubsequence; consider n being Nat such that A1: dom q c= Seg n by FINSEQ_1:def 12; defpred P[object,object] means ex k st k = $1 & $2 = i+k; A2: for x being object st x in dom q ex y being object st P[x,y] proof let x be object; assume x in dom q; then reconsider x as Element of NAT; take i+x; thus thesis; end; consider f being Function such that A3: dom f = dom q and A4: for x being object st x in dom q holds P[x, f.x] from CLASSES1:sch 1(A2); reconsider ss = f as FinSubsequence by A1,A3,FINSEQ_1:def 12; A5: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12; A6: rng ss = dom Shift(q,i) proof thus rng ss c= dom Shift(q,i) proof let y be object; assume y in rng ss; then consider x being object such that A7: x in dom ss and A8: y = ss.x by FUNCT_1:def 3; ex k1 st ( k1 = x)&( ss.x = i+k1) by A3,A4,A7; hence thesis by A3,A5,A7,A8; end; let y be object; assume y in dom Shift(q,i); then consider k2 being Nat such that A9: y = k2+i and A10: k2 in dom q by A5; ex k3 being Element of NAT st ( k3 = k2)&( ss.k2 = i+k3) by A4,A10; hence thesis by A3,A9,A10,FUNCT_1:def 3; end; A11: for k st k in dom q holds ss.k = i+k proof let k; assume k in dom q; then ex k1 st ( k1 = k)&( ss.k = i+k1) by A4; hence thesis; end; for x1,x2 being object st x1 in dom ss & x2 in dom ss & ss.x1 = ss.x2 holds x1 = x2 proof let x1,x2 be object; assume that A12: x1 in dom ss and A13: x2 in dom ss and A14: ss.x1 = ss.x2; A15: ex k1 st ( k1 = x1)&( ss.x1 = i+k1) by A3,A4,A12; ex k2 st ( k2 = x2)&( ss.x2 = i+k2) by A3,A4,A13; hence thesis by A14,A15; end; then ss is one-to-one; hence thesis by A3,A6,A11; end; Lm5: for p being FinSequence holds ex fs being FinSequence st dom fs = dom p & rng fs = dom Shift(p,i) & (for k st k in dom p holds fs.k = i+k) & fs is one-to-one proof let p be FinSequence; consider ss being FinSubsequence such that A1: dom ss = dom p and A2: rng ss = dom Shift(p,i) and A3: for k st k in dom p holds ss.k = i+k and A4: ss is one-to-one by Th40; dom ss = Seg len p by A1,FINSEQ_1:def 3; then reconsider fs = ss as FinSequence by FINSEQ_1:def 2; dom fs = dom p by A1; hence thesis by A2,A3,A4; end; theorem Th41: for q being FinSubsequence holds card q = card Shift(q,i) proof let q be FinSubsequence; ex ss being FinSubsequence st ( dom ss = dom q)&( rng ss = dom Shift(q,i))&( for k st k in dom q holds ss.k = i+k)&( ss is one-to-one) by Th40; then A1: dom q, dom Shift(q,i) are_equipotent; A2: card dom q = card q by CARD_1:62; card dom Shift(q,i) = card Shift(q,i) by CARD_1:62; hence thesis by A1,A2,CARD_1:5; end; theorem Th42: for p being FinSequence holds dom p = dom Seq Shift(p,i) proof let p be FinSequence; A1: rng Sgm dom Shift(p,i) = dom Shift(p,i) by FINSEQ_1:50; A2: dom p = Seg len p by FINSEQ_1:def 3; A3: dom Sgm dom Shift(p,i) = Seg len Sgm dom Shift(p,i) by FINSEQ_1:def 3; ex k be Nat st ( dom Shift(p,i) c= Seg k) by FINSEQ_1:def 12; then A4: len Sgm dom Shift(p,i) = card dom Shift(p,i) by FINSEQ_3:39; card dom Shift(p,i) = card Shift(p,i) by CARD_1:62; then card dom Shift(p,i) = len p by Th41; hence thesis by A1,A2,A3,A4,RELAT_1:27; end; theorem Th43: for p being FinSequence st k in dom p holds (Sgm dom Shift(p,i)).k = i + k proof let p be FinSequence; assume A1: k in dom p; consider fs being FinSequence such that A2: dom fs = dom p and A3: rng fs = dom Shift(p,i) and A4: for j st j in dom p holds fs.j = i+j and fs is one-to-one by Lm5; A5: ex l be Nat st ( dom Shift(p,i) c= Seg l) by FINSEQ_1:def 12; reconsider fs as FinSequence of NAT by A3,FINSEQ_1:def 4; for n,m,k1,k2 being Nat st 1 <= n & n < m & m <= len fs & k1 = fs.n & k2 = fs.m holds k1 < k2 proof let n,m,k1,k2 be Nat; assume that A6: 1 <= n and A7: n < m and A8: m <= len fs and A9: k1 = fs.n and A10: k2 = fs.m; reconsider n,m as Element of NAT by ORDINAL1:def 12; A11: dom fs = Seg len fs by FINSEQ_1:def 3 .= {n1 where n1 is Nat: 1 <= n1 & n1 <= len fs}; n+1 <= m by A7,INT_1:7; then n+1 <= len fs by A8,XXREAL_0:2; then A12: n <= (len fs) - 1 by XREAL_1:19; (len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7; then (len fs) - 1 <= len fs by XREAL_1:20; then n <= len fs by A12,XXREAL_0:2; then A13: n in dom p by A2,A6,A11; 1 <= m by A6,A7,XXREAL_0:2; then A14: m in dom p by A2,A8,A11; A15: k1 = i+n by A4,A9,A13; k2 = i+m by A4,A10,A14; hence thesis by A7,A15,XREAL_1:8; end; then fs = Sgm dom Shift(p,i) by A3,A5,FINSEQ_1:def 13; hence thesis by A1,A4; end; theorem Th44: for p being FinSequence st k in dom p holds (Seq Shift(p,i)).k = p.k proof let p be FinSequence; assume A1: k in dom p; then A2: k in dom Seq Shift(p,i) by Th42; (Shift(p,i)*(Sgm dom Shift(p,i))).k = Shift(p,i).((Sgm dom Shift(p,i)).k) by A2,FUNCT_1:12 .= Shift(p,i).(i+k) by A1,Th43; hence thesis by A1,Def12; end; theorem for p being FinSequence holds Seq Shift(p,i) = p proof let p be FinSequence; A1: dom Seq Shift(p,i) = dom p by Th42; for x being object holds x in dom p implies (Seq Shift(p,i)).x = p.x by Th44; hence thesis by A1; end; reserve p1,p2 for FinSequence; Lm6: for j,k,l being Nat st 1 <= j & j <= l or l+1 <= j & j <= l+k holds 1 <= j & j <= l+k proof let j,k,l be Nat; assume that A1: 1 <= j & j <= l or l+1 <= j & j <= l+k; per cases by A1; suppose A2: 1 <= j & j <= l; l+(0 qua Nat) <= l+k by XREAL_1:7; hence thesis by A2,XXREAL_0:2; end; suppose A3: l+1 <= j & j <= l+k; 0 qua Nat+1 <= l+1 by XREAL_1:7; hence thesis by A3,XXREAL_0:2; end; end; theorem Th46: dom (p1 \/ Shift(p2,len p1)) = Seg (len p1 + len p2) proof A1: dom (p1 \/ Shift(p2,len p1)) = dom p1 \/ dom (Shift(p2,len p1)) by XTUPLE_0:23; A2: dom p1 = Seg len p1 by FINSEQ_1:def 3 .= {k where k is Nat: 1 <= k & k <= len p1}; A3: dom (Shift(p2,len p1)) = {k1 where k1 is Nat: len p1 + 1 <= k1 & k1 <= len p1 + len p2} by Th39; thus dom (p1 \/ Shift(p2,len p1)) c= Seg (len p1 + len p2) proof let x be object; assume x in dom (p1 \/ (Shift(p2,len p1))); then A4: x in dom p1 or x in dom (Shift(p2,len p1)) by A1,XBOOLE_0:def 3; then A5: ex k3 being Nat st x = k3 & 1 <= k3 & k3 <= len p1 or x = k3 & len p1 + 1 <= k3 & k3 <= len p1 + len p2 by A2,A3; reconsider x as Nat by A4; A6: 1 <= x by A5,Lm6; x <= len p1 + len p2 by A5,Lm6; hence thesis by A6; end; let x be object; assume x in Seg (len p1 + len p2); then consider j being Nat such that A7: x = j and A8: 1 <= j and A9: j <= len p1 + len p2; reconsider i0 = len p1 as Integer; 1 <= j & j <= i0 or i0 + 1 <= j & j <= i0 + len p2 by A8,A9,INT_1:7; then x in dom p1 or x in dom Shift(p2,len p1) by A2,A3,A7; hence thesis by A1,XBOOLE_0:def 3; end; theorem Th47: for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds dom p1 misses dom Shift(p2,i) proof let p1 be FinSequence, p2 be FinSubsequence; assume A1: len p1 <= i; A2: dom p1 = Seg len p1 by FINSEQ_1:def 3 .= {k where k is Nat: 1 <= k & k <= len p1}; A3: dom Shift(p2,i) = {k+i where k is Nat: k in dom p2} by Def12; not ex x being object st x in dom p1 /\ dom Shift(p2,i) proof given x being object such that A4: x in dom p1 /\ dom Shift(p2,i); A5: x in dom p1 by A4,XBOOLE_0:def 4; A6: x in dom Shift(p2,i) by A4,XBOOLE_0:def 4; A7: ex k1 being Nat st ( x = k1)&( 1 <= k1)&( k1 <= len p1) by A2,A5; consider k2 being Nat such that A8: x = k2+i and A9: k2 in dom p2 by A3,A6; consider n being Nat such that A10: dom p2 c= Seg n by FINSEQ_1:def 12; A11: k2 in Seg n by A9,A10; A12: ex m being Nat st k2 = m & 1 <= m & m <= n by A11; reconsider x as Element of NAT by A4; len p1 + k2 <= i+k2 by A1,XREAL_1:7; then (len p1 + k2) - k2 < x - 0 by A8,A12,XREAL_1:15; hence contradiction by A7; end; hence dom p1 /\ dom Shift(p2,i) = {} by XBOOLE_0:def 1; end; theorem for p1,p2 being FinSequence holds p1^p2 = p1 \/ (Shift(p2,len p1)) proof let p1,p2; A1: dom (p1 \/ (Shift(p2,len p1))) = Seg (len p1 + len p2) by Th46; dom p1 misses dom (Shift(p2,len p1)) by Th47; then reconsider p = p1 \/ (Shift(p2,len p1)) as FinSequence by A1, FINSEQ_1:def 2,GRFUNC_1:13; A2: dom p = Seg (len p1 + len p2) by Th46; A3: for k be Nat st k in dom p1 holds p.k = p1.k proof let k be Nat; assume k in dom p1; then [k,p1.k] in p1 by FUNCT_1:def 2; then [k,p1.k] in p by XBOOLE_0:def 3; hence thesis by FUNCT_1:1; end; for k be Nat st k in dom p2 holds p.(len p1 + k) = p2.k proof let k be Nat; assume A4: k in dom p2; dom (Shift(p2,len p1)) = {j+len p1 where j is Nat: j in dom p2} by Def12; then len p1 + k in dom (Shift(p2,len p1)) by A4; then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in (Shift(p2,len p1)) by FUNCT_1:def 2; then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in p by XBOOLE_0:def 3; then p.(len p1 + k) = (Shift(p2,len p1)).(len p1 + k) by FUNCT_1:1; hence thesis by A4,Def12; end; hence thesis by A2,A3,FINSEQ_1:def 7; end; theorem for p1 being FinSequence, p2 being FinSubsequence st i >= len p1 holds p1 misses Shift(p2,i) proof let p1 be FinSequence, p2 be FinSubsequence; assume i >= len p1; then dom p1 misses dom Shift(p2,i) by Th47; hence thesis by RELAT_1:179 ; end; theorem for F being total NAT-defined Function, p be NAT-defined Function, n be Element of NAT st Shift(p,n) c= F for i being Element of NAT st i in dom p holds F.(n+i) = p.i proof let F be total NAT-defined Function, p be NAT-defined Function, n be Element of NAT such that A1: Shift(p,n) c= F; let i be Element of NAT; assume A2: i in dom p; then n+i in dom Shift(p,n) by Th24; hence F.(n+i) = Shift(p,n).(n+i) by A1,GRFUNC_1:2 .= p.i by A2,Def12; end; theorem Th51: for p,q being FinSubsequence st q c= p holds Shift(q,i) c= Shift(p,i) proof let p,q be FinSubsequence; assume A1: q c= p; A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12; A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12; let x,y be object; assume A4: [x,y] in Shift(q,i); then A5: x in dom Shift(q,i) by FUNCT_1:1; A6: y = Shift(q,i).x by A4,FUNCT_1:1; consider k being Nat such that A7: x = k+i and A8: k in dom q by A2,A5; A9: dom q c= dom p by A1,GRFUNC_1:2; then A10: x in dom Shift(p,i) by A3,A7,A8; y = q.k by A6,A7,A8,Def12 .= p.k by A1,A8,GRFUNC_1:2 .= Shift(p,i).x by A7,A8,A9,Def12; hence thesis by A10,FUNCT_1:1; end; theorem for p1,p2 being FinSequence holds Shift(p2,len p1) c= p1^p2 proof let p1,p2 be FinSequence; A1: dom Shift(p2,len p1) = {k+len p1 where k is Nat: k in dom p2} by Def12; A2: dom Shift(p2,len p1) = {k where k is Nat: len p1 + 1 <= k & k <= len p1 + len p2} by Th39; A3: dom (p1^p2) = Seg (len p1 + len p2) by FINSEQ_1:def 7 .= {k where k is Nat: 1 <= k & k <= len p1 + len p2}; let x,y be object; assume A4: [x,y] in Shift(p2,len p1); then A5: x in dom Shift(p2,len p1) by FUNCT_1:1; A6: y = Shift(p2,len p1).x by A4,FUNCT_1:1; consider k being Nat such that A7: x = k and A8: len p1 + 1 <= k and A9: k <= len p1 + len p2 by A2,A5; 1 <= len p1 + 1 by INT_1:6; then 1 <= k by A8,XXREAL_0:2; then A10: x in dom (p1^p2) by A3,A7,A9; consider j being Nat such that A11: x = j+len p1 and A12: j in dom p2 by A1,A5; y = p2.j by A6,A11,A12,Def12 .= (p1^p2).x by A11,A12,FINSEQ_1:def 7; hence thesis by A10,FUNCT_1:1; end; reserve q,q1,q2,q3,q4 for FinSubsequence, p1,p2 for FinSequence; theorem Th53: dom q1 misses dom q2 implies dom Shift(q1,i) misses dom Shift(q2,i) proof assume A1: dom q1 misses dom q2; A2: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12; A3: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12; now given x being object such that A4: x in dom Shift(q1,i) /\ dom Shift(q2,i); A5: x in dom Shift(q1,i) by A4,XBOOLE_0:def 4; A6: x in dom Shift(q2,i) by A4,XBOOLE_0:def 4; A7: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A2,A5; consider k2 being Nat such that A8: x = k2+i and A9: k2 in dom q2 by A3,A6; k2 in dom q1 /\ dom q2 by A7,A8,A9,XBOOLE_0:def 4; hence contradiction by A1; end; hence dom Shift(q1,i) /\ dom Shift(q2,i) = {} by XBOOLE_0:def 1; end; theorem for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds Shift(q1,i) \/ Shift(q2,i) = Shift(q,i) proof let q,q1,q2 be FinSubsequence such that A1: q = q1 \/ q2 and A2: q1 misses q2; A3: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12; A4: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12; A5: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12; A6: q1 c= q by A1,XBOOLE_1:7; A7: q2 c= q by A1,XBOOLE_1:7; A8: Shift(q1,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7; A9: Shift(q2,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7; dom q1 misses dom q2 by A2,A6,A7,FUNCT_1:112; then dom Shift(q1,i) misses dom Shift(q2,i) by Th53; then reconsider q3 = Shift(q1,i) \/ Shift(q2,i) as Function by GRFUNC_1:13; let x,y be object; thus [x,y] in Shift(q1,i) \/ Shift(q2,i) implies [x,y] in Shift(q,i) proof assume A10: [x,y] in Shift(q1,i) \/ Shift(q2,i); then x in dom q3 by FUNCT_1:1; then A11: x in dom Shift(q1,i) \/ dom Shift(q2,i) by XTUPLE_0:23; A12: now assume A13: x in dom Shift(q1,i); A14: dom Shift(q1,i) c= dom Shift(q,i) by A8,GRFUNC_1:2; Shift(q1,i).x = Shift(q,i).x by A8,A13,GRFUNC_1:2; then [x,Shift(q,i).x] in Shift(q1,i) by A13,FUNCT_1:def 2; then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3; hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A13,A14,FUNCT_1:def 1 ; end; now assume A15: x in dom Shift(q2,i); A16: dom Shift(q2,i) c= dom Shift(q,i) by A9,GRFUNC_1:2; Shift(q2,i).x = Shift(q,i).x by A9,A15,GRFUNC_1:2; then [x,Shift(q,i).x] in Shift(q2,i) by A15,FUNCT_1:def 2; then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3; hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A15,A16,FUNCT_1:def 1 ; end; hence thesis by A11,A12,FUNCT_1:1,XBOOLE_0:def 3; end; assume A17: [x,y] in Shift(q,i); then A18: x in dom Shift(q,i) by FUNCT_1:1; A19: y = Shift(q,i).x by A17,FUNCT_1:1; consider k being Nat such that A20: x = k+i and A21: k in dom q by A3,A18; dom q = dom q1 \/ dom q2 by A1,XTUPLE_0:23; then A22: k in dom q1 or k in dom q2 by A21,XBOOLE_0:def 3; then x in dom Shift(q1,i) or x in dom Shift(q2,i) by A4,A5,A20; then x in dom Shift(q1,i) \/ dom Shift(q2,i) by XBOOLE_0:def 3; then A23: x in dom q3 by XTUPLE_0:23; A24: now assume A25: x in dom Shift(q1,i); then A26: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A4; thus y = q.k by A19,A20,A21,Def12 .= q1.k by A1,A20,A26,GRFUNC_1:15 .= Shift(q1,i).x by A20,A26,Def12 .= q3.x by A25,GRFUNC_1:15; end; now assume A27: x in dom Shift(q2,i); then A28: ex k2 being Nat st ( x = k2+i)&( k2 in dom q2) by A5; thus y = q.k by A19,A20,A21,Def12 .= q2.k by A1,A20,A28,GRFUNC_1:15 .= Shift(q2,i).x by A20,A28,Def12 .= q3.x by A27,GRFUNC_1:15; end; hence thesis by A4,A5,A20,A22,A23,A24,FUNCT_1:1; end; theorem Th55: for q being FinSubsequence holds dom Seq q = dom Seq Shift(q,i) proof let q be FinSubsequence; A1: len Seq q = card q by FINSEQ_3:158; A2: len Seq Shift(q,i) = card Shift(q,i) by FINSEQ_3:158; thus dom Seq q = Seg len Seq q by FINSEQ_1:def 3 .= dom Seq Shift(q,i) by Th41,A1,A2,FINSEQ_1:def 3; end; reserve l1 for Nat, j2 for Element of NAT; theorem Th56: for q being FinSubsequence st k in dom Seq q ex j st j = (Sgm dom q).k & (Sgm dom Shift(q,i)).k = i + j proof let q be FinSubsequence such that A1: k in dom Seq q; consider ss being FinSubsequence such that A2: dom ss = dom q and A3: rng ss = dom Shift(q,i) and A4: for l st l in dom q holds ss.l = i+l and ss is one-to-one by Th40; A5: rng Seq ss = dom Shift(q,i) by A3,FINSEQ_1:101; A6: rng Sgm dom q = dom q by FINSEQ_1:50; A7: dom Seq q = dom (q*Sgm dom q) .= dom Sgm dom q by A6,RELAT_1:27; A8: for l1 st l1 in dom Seq q ex j1 st j1 = (Sgm dom q).l1 & (Seq ss).l1 = i+j1 proof let l1 such that A9: l1 in dom Seq q; A10: (Sgm dom q).l1 in rng Sgm dom q by A7,A9,FUNCT_1:def 3; then A11: (Sgm dom q).l1 in dom q by FINSEQ_1:50; reconsider j1 = (Sgm dom q).l1 as Element of NAT by A10; (Seq ss).l1 = (ss*Sgm dom ss).l1 .= ss.j1 by A2,A7,A9,FUNCT_1:13 .= i+j1 by A4,A11; hence thesis; end; A12: rng ss = rng Sgm dom Shift(q,i) by A3,FINSEQ_1:50; rng Sgm dom Shift(q,i) c= NAT; then rng Seq ss c= NAT by A12,FINSEQ_1:101; then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def 4; A13: ex l2 be Nat st ( dom Shift(q,i) c= Seg l2) by FINSEQ_1:def 12; A14: dom Seq ss = dom (ss*Sgm dom ss) .= dom Sgm dom q by A2,A6,RELAT_1:27; for n,m,k1,k2 being Nat st 1 <= n & n < m & m <= len fs & k1 = fs.n & k2 = fs.m holds k1 < k2 proof let n,m,k1,k2 be Nat; assume that A15: 1 <= n and A16: n < m and A17: m <= len fs and A18: k1 = fs.n and A19: k2 = fs.m; reconsider n,m as Element of NAT by ORDINAL1:def 12; A20: dom fs = Seg len fs by FINSEQ_1:def 3 .= {l3 where l3 is Nat: 1 <= l3 & l3 <= len fs}; n+1 <= m by A16,INT_1:7; then n+1 <= len fs by A17,XXREAL_0:2; then A21: n <= (len fs) - 1 by XREAL_1:19; (len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7; then (len fs) - 1 <= len fs by XREAL_1:20; then n <= len fs by A21,XXREAL_0:2; then A22: n in dom Seq q by A7,A14,A15,A20; 1 <= m by A15,A16,XXREAL_0:2; then A23: m in dom Seq q by A7,A14,A17,A20; consider j2 being Element of NAT such that A24: j2 = (Sgm dom q).n and A25: fs.n = i+j2 by A8,A22; consider j3 being Element of NAT such that A26: j3 = (Sgm dom q).m and A27: fs.m = i+j3 by A8,A23; A28: ex l3 being Nat st ( dom q c= Seg l3) by FINSEQ_1:def 12; dom Seq ss = Seg len fs by FINSEQ_1:def 3; then len fs = len Sgm dom q by A14,FINSEQ_1:def 3; then j2 < j3 by A15,A16,A17,A24,A26,A28,FINSEQ_1:def 13; hence thesis by A18,A19,A25,A27,XREAL_1:8; end; then fs = Sgm dom Shift(q,i) by A5,A13,FINSEQ_1:def 13; hence thesis by A1,A8; end; theorem Th57: for q being FinSubsequence st k in dom Seq q holds (Seq Shift(q,i)).k = (Seq q).k proof let q be FinSubsequence; assume A1: k in dom Seq q; then consider j such that A2: j = (Sgm dom q).k and A3: (Sgm dom Shift(q,i)).k = i+j by Th56; A4: rng Sgm dom q = dom q by FINSEQ_1:50; A5: dom Seq q = dom Seq Shift(q,i) by Th55 .= dom (Shift(q,i)*(Sgm dom Shift(q,i))); A6: dom Seq q = dom (q*Sgm dom q) .= dom Sgm dom q by A4,RELAT_1:27; then j in rng Sgm dom q by A1,A2,FUNCT_1:def 3; then A7: j in dom q by FINSEQ_1:50; (Seq Shift(q,i)).k = (Shift(q,i)*(Sgm dom Shift(q,i))).k .= Shift(q,i).((Sgm dom Shift(q,i)).k) by A1,A5,FUNCT_1:12 .= q.j by A3,A7,Def12 .= (q*Sgm dom q).k by A1,A2,A6,FUNCT_1:13 .= (Seq q).k; hence thesis; end; theorem for q being FinSubsequence holds Seq q = Seq Shift(q,i) proof let q be FinSubsequence; A1: dom Seq q = dom Seq Shift(q,i) by Th55; for x being object holds x in dom Seq q implies (Seq Shift(q,i)).x = (Seq q).x by Th57; hence thesis by A1; end; theorem Th59: for q being FinSubsequence st dom q c= Seg k holds dom Shift(q,i) c= Seg (i+k) proof let q be FinSubsequence; assume A1: dom q c= Seg k; A2: dom Shift(q,i) = {j+i where j is Nat: j in dom q} by Def12; let x be object; assume x in dom Shift(q,i); then consider j1 being Nat such that A3: x = j1+i and A4: j1 in dom q by A2; j1 in Seg k by A1,A4; then A5: ex j2 being Nat st ( j1 = j2)&( 1 <= j2)&( j2 <= k); A6: 0 qua Nat+1 <= i+j1 by A5,XREAL_1:7; i+j1 <= i+k by A5,XREAL_1:7; hence thesis by A3,A6; end; theorem Th60: for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p) proof let p be FinSequence, q1,q2 be FinSubsequence; assume q1 c= p; then A1: dom q1 c= dom p by GRFUNC_1:2; dom p misses dom Shift(q2,len p) by Th47; then reconsider ss = q1 \/ Shift(q2,len p) as Function by A1,GRFUNC_1:13 ,XBOOLE_1:63; A2: dom p = Seg len p by FINSEQ_1:def 3; consider k be Nat such that A3: dom q2 c= Seg k by FINSEQ_1:def 12; k in NAT by ORDINAL1:def 12; then A4: dom Shift(q2,len p) c= Seg (len p + k) by A3,Th59; len p + (0 qua Nat) <= len p + k by XREAL_1:7; then Seg len p c= Seg (len p + k) by FINSEQ_1:5; then dom q1 c= Seg (len p + k) by A1,A2; then dom q1 \/ dom Shift(q2,len p) c= Seg (len p + k) by A4,XBOOLE_1:8; then dom (q1 \/ Shift(q2,len p)) c= Seg (len p + k) by XTUPLE_0:23; then reconsider ss as FinSubsequence by FINSEQ_1:def 12; take ss; thus thesis; end; Lm7: for p,q being FinSubsequence st q c= p holds dom Shift(q,i) c= dom Shift(p,i) proof let p,q be FinSubsequence; assume A1: q c= p; A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12; A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12; A4: dom q c= dom p by A1,GRFUNC_1:2; let x be object; assume x in dom Shift(q,i); then ex k1 being Nat st ( x = k1+i)&( k1 in dom q) by A2; hence thesis by A3,A4; end; Lm8: for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds Sgm (dom q1 \/ dom Shift(q2,len p1)) = (Sgm dom q1)^(Sgm dom Shift(q2,len p1)) proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume that A1: q1 c= p1 and A2: q2 c= p2; A3: ex k1 be Nat st ( dom q1 c= Seg k1) by FINSEQ_1:def 12; A4: ex k2 be Nat st ( dom Shift(q2,len p1) c= Seg k2) by FINSEQ_1:def 12; for m,n being Nat st m in dom q1 & n in dom Shift(q2,len p1) holds m < n proof let m,n be Nat such that A5: m in dom q1 and A6: n in dom Shift(q2,len p1); A7: dom p1 = Seg len p1 by FINSEQ_1:def 3 .= {k where k is Nat: 1 <= k & k <= len p1}; A8: dom Shift(p2,len p1) = {k where k is Nat : len p1 + 1 <= k & k <= len p1 + len p2} by Th39; A9: dom q1 c= dom p1 by A1,GRFUNC_1:2; A10: dom Shift(q2,len p1) c= dom Shift(p2,len p1) by A2,Lm7; A11: m in dom p1 by A5,A9; A12: n in dom Shift(p2,len p1) by A6,A10; consider k3 being Nat such that A13: k3 = m and 1 <= k3 and A14: k3 <= len p1 by A7,A11; consider k4 being Nat such that A15: k4 = n and A16: len p1 + 1 <= k4 and k4 <= len p1 + len p2 by A8,A12; len p1 < len p1 + 1 by XREAL_1:29; then k3 <= len p1 + 1 by A14,XXREAL_0:2; then A17: k3 <= k4 by A16,XXREAL_0:2; k3 <> k4 by A5,A6,A9,A13,A15,Th47,XBOOLE_0:3; hence thesis by A13,A15,A17,XXREAL_0:1; end; hence thesis by A3,A4,FINSEQ_3:42; end; theorem Th61: for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2 ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) & dom Seq ss = Seg (len Seq q1 + len Seq q2) proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume that A1: q1 c= p1 and A2: q2 c= p2; consider ss being FinSubsequence such that A3: ss = q1 \/ Shift(q2,len p1) by A1,Th60; A4: ex k1 be Nat st ( dom q1 c= Seg k1) by FINSEQ_1:def 12; A5: ex k2 be Nat st ( dom Shift(q2,len p1) c= Seg k2) by FINSEQ_1:def 12; A6: rng Sgm dom ss = dom ss by FINSEQ_1:50; A7: dom Seq ss = dom Sgm dom ss by A6,RELAT_1:27 .= dom Sgm (dom q1 \/ dom Shift(q2,len p1)) by A3,XTUPLE_0:23 .= dom ((Sgm dom q1)^(Sgm dom Shift(q2,len p1))) by A1,A2,Lm8 .= Seg (len Sgm dom q1 + len Sgm dom Shift(q2,len p1)) by FINSEQ_1:def 7; A8: len Sgm dom Shift(q2,len p1) = card dom Shift(q2,len p1) by A5,FINSEQ_3:39; A9: len Sgm dom q1 = card dom q1 by A4,FINSEQ_3:39; len Sgm dom Shift(q2,len p1) = card Shift(q2,len p1) by A8,CARD_1:62; then A10: len Sgm dom Shift(q2,len p1) = card q2 by Th41; A11: len Sgm dom q1 = card q1 by A9,CARD_1:62; A12: len Sgm dom Shift(q2,len p1) = len Seq q2 by A10,FINSEQ_3:158; len Sgm dom q1 = len Seq q1 by A11,FINSEQ_3:158; hence thesis by A3,A7,A12; end; theorem Th62: for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2 ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) & dom Seq ss = Seg (len Seq q1 + len Seq q2) & Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1) proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume that A1: q1 c= p1 and A2: q2 c= p2; consider ss being FinSubsequence such that A3: ss = q1 \/ Shift(q2,len p1) and A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) by A1,A2,Th61; A5: dom Seq q1 = Seg len Seq q1 by FINSEQ_1:def 3 .= {k where k is Nat: 1 <= k & k <= len Seq q1}; A6: dom Shift(Seq q2,len Seq q1) = {k where k is Nat: len Seq q1 + 1 <= k & k <= len Seq q1 + len Seq q2} by Th39; A7: Seg (len Seq q1 + len Seq q2) = dom Seq q1 \/ dom Shift(Seq q2,len Seq q1) proof thus Seg (len Seq q1 + len Seq q2) c= dom Seq q1 \/ dom Shift(Seq q2,len Seq q1) proof let x be object; assume x in Seg (len Seq q1 + len Seq q2); then consider k1 being Nat such that A8: x = k1 and A9: 1 <= k1 and A10: k1 <= len Seq q1 + len Seq q2; A11: 1 <= k1 & k1 <= len Seq q1 implies k1 in dom Seq q1 by A5; len Seq q1 + 1 <= k1 & k1 <= len Seq q1 + len Seq q2 implies k1 in dom Shift(Seq q2,len Seq q1) by A6; hence thesis by A8,A9,A10,A11,INT_1:7,XBOOLE_0:def 3; end; let x be object; assume A12: x in dom Seq q1 \/ dom Shift(Seq q2,len Seq q1); A13: now assume x in dom Seq q1; then consider k1 being Nat such that A14: x = k1 and A15: 1 <= k1 and A16: k1 <= len Seq q1 by A5; len Seq q1 + (0 qua Nat) <= len Seq q1 + len Seq q2 by XREAL_1:7; then k1 <= len Seq q1 + len Seq q2 by A16,XXREAL_0:2; hence thesis by A14,A15; end; now assume x in dom Shift(Seq q2,len Seq q1); then consider k2 being Nat such that A17: x = k2 and A18: len Seq q1 + 1 <= k2 and A19: k2 <= len Seq q1 + len Seq q2 by A6; 0 qua Nat+1 <= len Seq q1 + 1 by XREAL_1:7; then 1 <= k2 by A18,XXREAL_0:2; hence thesis by A17,A19; end; hence thesis by A12,A13,XBOOLE_0:def 3; end; A20: dom Seq q1 \/ dom Shift(Seq q2,len Seq q1) = dom (Seq q1 \/ Shift(Seq q2,len Seq q1)) by XTUPLE_0:23; dom Seq q1 misses dom Shift(Seq q2,len Seq q1) by Th47; then reconsider ss1 = Seq q1 \/ Shift(Seq q2,len Seq q1) as Function by GRFUNC_1:13; for x being object st x in dom Seq ss holds (Seq ss).x = ss1.x proof let x be object; assume A21: x in dom Seq ss; A22: (Seq ss).x = (ss*Sgm dom ss).x .= ss.((Sgm dom ss).x) by A21,FUNCT_1:12 .= ss.((Sgm (dom q1 \/ dom Shift(q2,len p1))).x) by A3,XTUPLE_0:23 .= ss.(((Sgm dom q1)^(Sgm dom Shift(q2,len p1))).x) by A1,A2,Lm8; A23: now assume A24: x in dom Seq q1; then A25: x in dom Sgm dom q1 by FINSEQ_1:100; then (Sgm dom q1).x in rng Sgm dom q1 by FUNCT_1:def 3; then A26: (Sgm dom q1).x in dom q1 by FINSEQ_1:50; (Seq ss).x = ss.((Sgm dom q1).x) by A22,A25,FINSEQ_1:def 7 .= q1.((Sgm dom q1).x) by A3,A26,GRFUNC_1:15 .= (q1*Sgm dom q1).x by A25,FUNCT_1:13 .= (Seq q1).x; hence thesis by A24,GRFUNC_1:15; end; now assume A27: x in dom Shift(Seq q2,len Seq q1); dom Shift(Seq q2,len Seq q1) = {j+len Seq q1 where j is Nat: j in dom Seq q2 } by Def12; then consider j being Nat such that A28: x = j+len Seq q1 and A29: j in dom Seq q2 by A27; A30: ss1.x = Shift(Seq q2,len Seq q1).x by A27,GRFUNC_1:15 .= (Seq q2).j by A28,A29,Def12; A31: ex l1 be Nat st ( dom q1 c= Seg l1) by FINSEQ_1:def 12; A32: ex l2 be Nat st ( dom Shift(q2,len p1) c= Seg l2) by FINSEQ_1:def 12; card dom q1 = len Sgm dom q1 by A31,FINSEQ_3:39; then A33: card q1 = len Sgm dom q1 by CARD_1:62; A34: len Seq q1 = card q1 by FINSEQ_3:158; A35: dom Seq q2 = Seg len Seq q2 by FINSEQ_1:def 3; card q2 = len Seq q2 by FINSEQ_3:158; then A36: card Shift(q2,len p1) = len Seq q2 by Th41; then A37: card dom Shift(q2,len p1) = len Seq q2 by CARD_1:62; A38: card dom Shift(q2,len p1) = len Sgm dom Shift(q2,len p1) by A32,FINSEQ_3:39; A39: len Sgm dom Shift(q2,len p1) = len Seq q2 by A32,A37,FINSEQ_3:39; A40: dom Seq q2 = dom Sgm dom Shift(q2,len p1) by A35,A36,A38,CARD_1:62 ,FINSEQ_1:def 3; A41: j in dom Sgm dom Shift(q2,len p1) by A29,A35,A39,FINSEQ_1:def 3; (Sgm dom Shift(q2,len p1)).j in rng Sgm dom Shift(q2,len p1) by A29,A40,FUNCT_1:def 3; then A42: (Sgm dom Shift(q2,len p1)).j in dom Shift(q2,len p1) by FINSEQ_1:50; (Seq ss).x = ss.((Sgm dom Shift(q2,len p1)).j) by A22,A28,A33,A34,A41, FINSEQ_1:def 7 .= Shift(q2,len p1).((Sgm dom Shift(q2,len p1)).j) by A3,A42,GRFUNC_1:15 .= (Shift(q2,len p1)*(Sgm dom Shift(q2,len p1))).j by A29,A40,FUNCT_1:13 .= (Seq Shift(q2,len p1)).j .= (Seq q2).j by A29,Th57; hence thesis by A30; end; hence thesis by A4,A7,A21,A23,XBOOLE_0:def 3; end; then Seq ss = ss1 by A4,A7,A20; hence thesis by A3,A4; end; theorem for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2 ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) & (Seq q1)^(Seq q2) = Seq ss proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume that A1: q1 c= p1 and A2: q2 c= p2; consider ss being FinSubsequence such that A3: ss = q1 \/ Shift(q2,len p1) and A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) and A5: Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1) by A1,A2,Th62; A6: for j1 be Nat st j1 in dom Seq q1 holds (Seq ss).j1 = (Seq q1).j1 by A5,GRFUNC_1:15; for j2 be Nat st j2 in dom Seq q2 holds (Seq ss).(len Seq q1 + j2) = (Seq q2).j2 proof let j2 be Nat; assume A7: j2 in dom Seq q2; dom Shift(Seq q2,len Seq q1) = {k+len Seq q1 where k is Nat: k in dom Seq q2} by Def12; then len Seq q1 + j2 in dom Shift(Seq q2,len Seq q1) by A7; hence (Seq ss).(len Seq q1 + j2) = Shift(Seq q2,len Seq q1).(len Seq q1 + j2) by A5,GRFUNC_1:15 .= (Seq q2).j2 by A7,Def12; end; then Seq ss = (Seq q1)^(Seq q2) by A4,A6,FINSEQ_1:def 7; hence thesis by A3; end; theorem for F being non empty NAT-defined finite Function holds card CutLastLoc F = card F -' 1 proof let F be non empty NAT-defined finite Function; A1: card F >= 0+1 by NAT_1:13; thus card CutLastLoc F = card F - 1 by Th37 .= card F -' 1 by A1,XREAL_1:233; end; theorem for F,G being non empty NAT-defined finite Function st dom F = dom G holds LastLoc F = LastLoc G; theorem for f being non empty NAT-defined finite Function holds Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y) proof let f be non empty NAT-defined finite Function; A1: dom f = dom(f +~ (x,y)) by FUNCT_4:99; A2: dom(Shift(f,i) +~ (x,y)) = dom Shift(f,i) by FUNCT_4:99 .= { m+i where m is Nat:m in dom(f +~ (x,y)) } by A1,Def12; for m being Nat st m in dom(f +~ (x,y)) holds (Shift(f,i) +~ (x,y)).(m+i) = (f +~ (x,y)).m proof let m be Nat; assume m in dom(f +~ (x,y)); then A3: m+i in dom(Shift(f,i) +~ (x,y)) by A2; then A4: m+i in dom Shift(f,i) by FUNCT_4:99; consider mm being Nat such that A5: m+i = mm+i and A6: mm in dom(f +~ (x,y)) by A2,A3; m = mm by A5; then m in dom(f +~ (x,y)) by A6; then A7: m in dom f by FUNCT_4:99; then A8: Shift(f,i).(m+i) = f.m by Def12; per cases; suppose A9: Shift(f,i).(m+i) = x; hence (Shift(f,i) +~ (x,y)).(m+i) = y by A4,FUNCT_4:106 .= (f +~ (x,y)).m by A7,FUNCT_4:106,A9,A8; end; suppose A10: Shift(f,i).(m+i) <> x; hence (Shift(f,i) +~ (x,y)).(m+i) = Shift(f,i).(m+i) by FUNCT_4:105 .= (f +~ (x,y)).m by A10,A8,FUNCT_4:105; end; end; hence Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y) by A2,Def12; end; theorem for F, G being non empty NAT-defined finite Function st dom F c= dom G holds LastLoc F <= LastLoc G by XXREAL_2:59;