Copyright (c) 1989 Association of Mizar Users
environ vocabulary FUNCT_1, ARYTM, RELAT_1, PARTFUN1, BOOLE, ARYTM_1, ABSVALUE, ARYTM_3, SEQ_1, ZF_REFLE; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, REAL_1, RELAT_1, FUNCT_1, ABSVALUE, RELSET_1, PARTFUN1, FUNCT_2; constructors REAL_1, ABSVALUE, FUNCT_2, PARTFUN1, MEMBERED, XBOOLE_0; clusters XREAL_0, RELSET_1, FUNCT_2, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions XREAL_0, PARTFUN1, RELAT_1; theorems FUNCT_1, TARSKI, ABSVALUE, FUNCT_2, SUBSET_1, PARTFUN1, RELSET_1, RELAT_1, CARD_1, XREAL_0, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes FUNCT_1, FUNCT_2, XBOOLE_0; begin reserve f for Function; reserve n,k,n1 for Nat; reserve r,p for real number; reserve x,y,z for set; definition mode Real_Sequence is Function of NAT,REAL; end; reserve seq,seq1,seq2,seq3,seq',seq1' for Real_Sequence; canceled 2; theorem Th3:f is Real_Sequence iff (dom f=NAT & for x st x in NAT holds f.x is real) proof thus f is Real_Sequence implies (dom f=NAT & for x st x in NAT holds f.x is real) proof assume A1: f is Real_Sequence; hence dom f=NAT by FUNCT_2:def 1; A2: rng f c=REAL by A1,RELSET_1:12; let x; assume x in NAT; then x in dom f by A1,FUNCT_2:def 1; then f.x in rng f by FUNCT_1:def 5; hence f.x in REAL by A2; end; assume that A3: dom f= NAT and A4: for x st x in NAT holds f.x is real; now let y; assume y in rng f; then consider x such that A5: x in dom f and A6: y=f.x by FUNCT_1:def 5; f.x is real by A3,A4,A5; hence y in REAL by A6,XREAL_0:def 1; end; then rng f c=REAL by TARSKI:def 3; hence thesis by A3,FUNCT_2:def 1,RELSET_1:11; end; theorem Th4:f is Real_Sequence iff (dom f=NAT & for n holds f.n is real) proof thus f is Real_Sequence implies (dom f=NAT & for n holds f.n is real) by Th3; assume that A1: dom f=NAT and A2: for n holds f.n is real; for x holds x in NAT implies f.x is real by A2; hence thesis by A1,Th3; end; definition let f be Relation; attr f is real-yielding means :Def1: rng f c= REAL; end; definition let C be set; cluster -> real-yielding PartFunc of C, REAL; coherence proof let f be PartFunc of C, REAL; thus rng f c= REAL; end; end; definition cluster real-yielding Function; existence proof consider A being set; consider f being Function of A, REAL; take f; thus rng f c= REAL; end; end; definition let f be real-yielding Function, x be set; cluster f.x -> real; coherence proof per cases; suppose x in dom f; then A1: f.x in rng f by FUNCT_1:12; rng f c= REAL by Def1; hence f.x in REAL by A1; suppose not x in dom f; hence thesis by CARD_1:51,FUNCT_1:def 4; end; end; definition let f be real-yielding Function, x be set; redefine func f.x -> Real; coherence by XREAL_0:def 1; end; definition let C be set, f be PartFunc of C, REAL, x be set; redefine func f.x -> Real; coherence by XREAL_0:def 1; end; definition let f be PartFunc of NAT, REAL; redefine attr f is non-empty means :Def2: rng f c= REAL \ {0}; compatibility proof thus f is non-empty implies rng f c= REAL \ {0} proof assume not {} in rng f; hence thesis by ZFMISC_1:40; end; assume rng f c= REAL \ {0}; then not {} in rng f by ZFMISC_1:64; hence thesis by RELAT_1:def 9; end; synonym f is being_not_0; synonym f is_not_0; end; canceled; theorem Th6: seq is being_not_0 iff for x st x in NAT holds seq.x<>0 proof thus seq is being_not_0 implies for x st x in NAT holds seq.x<>0 proof assume seq is being_not_0; then A1: rng seq c= REAL\{0} by Def2; let x; assume x in NAT; then x in dom seq by Th4; then seq.x in rng seq by FUNCT_1:def 5; then not seq.x in {0} by A1,XBOOLE_0:def 4; hence seq.x<>0 by TARSKI:def 1; end; assume A2: for x st x in NAT holds seq.x<>0; now let y; assume y in rng seq; then consider x such that A3: x in dom seq and A4: seq.x=y by FUNCT_1:def 5; y<>0 by A2,A3,A4; then not y in {0} by TARSKI:def 1; hence y in REAL\{0} by A4,XBOOLE_0:def 4; end; then rng seq c=REAL\{0} by TARSKI:def 3; hence thesis by Def2; end; theorem Th7: seq is being_not_0 iff for n holds seq.n<>0 proof thus seq is being_not_0 implies for n holds seq.n<>0 by Th6; assume for n holds seq.n<>0; then for x holds x in NAT implies seq.x<>0; hence thesis by Th6; end; theorem for seq,seq1 st (for x st x in NAT holds seq.x=seq1.x) holds seq=seq1 proof let seq,seq1 such that A1: for x st x in NAT holds seq.x=seq1.x; dom seq= NAT & dom seq1=NAT by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:9; end; canceled; theorem for r ex seq st rng seq={r} proof let r; consider f such that A1: dom f=NAT and A2: rng f={r} by FUNCT_1:15; now let x; assume x in {r}; then x=r by TARSKI:def 1; hence x in REAL by XREAL_0:def 1; end; then rng f c= REAL by A2,TARSKI:def 3; then reconsider f as Real_Sequence by A1,FUNCT_2:def 1,RELSET_1:11; take f; thus rng f = {r} by A2; end; scheme ExRealSeq{F(set)->real number}: ex seq st for n holds seq.n=F(n) proof defpred P[set,set] means ex n st n=$1 & $2=F(n); A1: now let x; assume x in NAT; then consider n such that A2: n=x; reconsider r2=F(n) as set; take y=r2; thus P[x,y] by A2; end; A3: for x,y,z st x in NAT & P[x,y] & P[x,z] holds y=z; consider f such that A4: dom f=NAT and A5: for x st x in NAT holds P[x,f.x] from FuncEx(A3,A1); now let x; assume x in NAT; then ex n st n=x & f.x=F(n) by A5; hence f.x is real; end; then reconsider f as Real_Sequence by A4,Th3; take seq=f; let n; ex k st k=n & seq.n=F(k) by A5; hence seq.n=F(n); end; :: :: BASIC OPERATIONS ON SEQUENCES :: scheme PartFuncExD'{D,C()->non empty set, P[set,set]}: ex f being PartFunc of D(),C() st (for d be Element of D() holds d in dom f iff (ex c be Element of C() st P[d,c])) & (for d be Element of D() st d in dom f holds P[d,f.d]) proof consider x being Element of C(); defpred X[Element of D(),Element of C()] means ((ex c be Element of C() st P[$1,c]) implies P[$1,$2]) & ((for c be Element of C() holds not P[$1,c]) implies $2=x); A1: for d be Element of D() ex z be Element of C() st X[d,z] ::: ((ex c be Element of C() st P[d,c]) implies P[d,z]) & ::: ((for c be Element of C() holds not P[d,c]) implies z=x) proof let d be Element of D(); (for c be Element of C() holds not P[d,c]) implies ex z st ((ex c be Element of C() st P[d,c]) implies P[d,z]) & ((for c be Element of C() holds not P[d,c]) implies z=x); hence thesis; end; consider g being Function of D(),C() such that A2: for d be Element of D() holds X[d,g.d] ::: ((ex c be Element of C() st P[d,c]) implies P[d,g.d]) & ::: ((for c be Element of C() holds not P[d,c]) implies g.d=x) from FuncExD(A1); A3: dom g = D() & rng g c= C() by FUNCT_2:def 1; defpred X[set] means ex c be Element of C() st P[$1,c]; consider X be set such that A4: for x holds x in X iff x in D() & X[x] :::& ex c be Element of C() st P[x,c] from Separation; for x holds x in X implies x in D() by A4; then reconsider X as Subset of D() by TARSKI:def 3; reconsider f=g|X as PartFunc of D(),C(); take f; thus for d be Element of D() holds d in dom f iff (ex c be Element of C() st P[d,c]) proof let d be Element of D(); dom f c= X by RELAT_1:87; hence d in dom f implies ex c be Element of C() st P[d,c] by A4; assume ex c be Element of C() st P[d,c]; then d in X & d in D() by A4; then d in dom g /\ X by A3,XBOOLE_0:def 3; hence thesis by RELAT_1:90; end; let d be Element of D(); assume A5: d in dom f; dom f c= X by RELAT_1:87; then ex c be Element of C() st P[d,c] by A4,A5; then P[d,g.d] by A2; hence thesis by A5,FUNCT_1:70; end; scheme LambdaPFD'{D,C()->non empty set, F(set)->Element of C(), P[set]}: ex f being PartFunc of D(),C() st (for d be Element of D() holds d in dom f iff P[d]) & (for d be Element of D() st d in dom f holds f.d = F(d)) proof defpred X[Element of D(),set] means P[$1] & $2 = F($1); consider f being PartFunc of D(),C() such that A1: for d be Element of D() holds d in dom f iff ex c be Element of C() st X[d,c] :::P[c,d] & c = F(d) and A2: for d be Element of D() st d in dom f holds X[d,f.d] :::P[d] & f.d = F(d) from PartFuncExD'; take f; thus for d be Element of D() holds d in dom f iff P[d] proof let d be Element of D(); thus d in dom f implies P[d] proof assume d in dom f; then ex c be Element of C() st P[d] & c = F(d) by A1; hence thesis; end; assume P[d]; then ex c be Element of C() st P[d] & c = F(d); hence thesis by A1; end; thus thesis by A2; end; scheme UnPartFuncD'{C,D,X() -> set, F(set)->set}: for f,g being PartFunc of C(),D() st (dom f=X() & for c be Element of C() st c in dom f holds f.c = F(c)) & (dom g=X() & for c be Element of C() st c in dom g holds g.c = F(c)) holds f = g proof let f,g be PartFunc of C(),D(); assume that A1: (dom f=X() & for c be Element of C() st c in dom f holds f.c = F(c)) and A2: dom g=X() & for c be Element of C() st c in dom g holds g.c = F(c); now let c be Element of C(); assume A3: c in dom f; hence f.c = F(c) by A1 .= g.c by A1,A2,A3; end; hence thesis by A1,A2,PARTFUN1:34; end; definition let C be :::non empty set; let f1,f2 be PartFunc of C,REAL; func f1+f2 -> PartFunc of C,REAL means :Def3: dom it = dom f1 /\ dom f2 & for c being Element of C st c in dom it holds it.c = f1.c + f2.c; existence proof per cases; suppose A1: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f1 /\ dom f2 by A1,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f1 /\ dom f2; deffunc U(Element of C') = f1.$1 + f2.$1; consider F be PartFunc of C',REAL such that A2: for c being Element of C' holds c in dom F iff X[c] and A3: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A2,SUBSET_1:8; thus thesis by A3; end; uniqueness proof deffunc U(Element of C) = f1.$1 + f2.$1; thus for f,g being PartFunc of C,REAL st (dom f=dom f1 /\ dom f2 & for c be Element of C st c in dom f holds f.c = U(c)) & (dom g=dom f1 /\ dom f2 & for c be Element of C st c in dom g holds g.c = U(c)) holds f = g from UnPartFuncD'; end; commutativity; func f1-f2 -> PartFunc of C,REAL means :Def4: dom it = dom f1 /\ dom f2 & for c being Element of C st c in dom it holds it.c = f1.c - f2.c; existence proof per cases; suppose A4: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f1 /\ dom f2 by A4,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f1 /\ dom f2; deffunc U(Element of C') = f1.$1 - f2.$1; consider F be PartFunc of C',REAL such that A5: for c being Element of C' holds c in dom F iff X[c] and A6: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A5,SUBSET_1:8; thus thesis by A6; end; uniqueness proof deffunc U(Element of C) = f1.$1 - f2.$1; thus for f,g being PartFunc of C,REAL st (dom f=dom f1 /\ dom f2 & for c be Element of C st c in dom f holds f.c = U(c)) & (dom g=dom f1 /\ dom f2 & for c be Element of C st c in dom g holds g.c = U(c)) holds f = g from UnPartFuncD'; end; func f1(#)f2 -> PartFunc of C,REAL means :Def5: dom it = dom f1 /\ dom f2 & for c being Element of C st c in dom it holds it.c = f1.c * f2.c; existence proof per cases; suppose A7: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f1 /\ dom f2 by A7,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f1 /\ dom f2; deffunc U(Element of C') = f1.$1 * f2.$1; consider F be PartFunc of C',REAL such that A8: for c being Element of C' holds c in dom F iff X[c] and A9: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A8,SUBSET_1:8; thus thesis by A9; end; uniqueness proof deffunc U(Element of C) = f1.$1 * f2.$1; thus for f,g being PartFunc of C,REAL st (dom f=dom f1 /\ dom f2 & for c be Element of C st c in dom f holds f.c = U(c)) & (dom g=dom f1 /\ dom f2 & for c be Element of C st c in dom g holds g.c = U(c)) holds f = g from UnPartFuncD'; end; commutativity; end; theorem Th11: seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n proof thus seq = seq1 + seq2 implies for n holds seq.n =seq1.n + seq2.n proof assume A1: seq = seq1 + seq2; let n; dom seq = NAT by FUNCT_2:def 1; hence seq.n =seq1.n + seq2.n by A1,Def3; end; assume A2: for n holds seq.n =seq1.n + seq2.n; A3: dom seq = NAT /\ NAT by FUNCT_2:def 1 .= NAT /\ dom seq2 by FUNCT_2:def 1 .= dom seq1 /\ dom seq2 by FUNCT_2:def 1; for n st n in dom seq holds seq.n = seq1.n + seq2.n by A2; hence thesis by A3,Def3; end; theorem Th12: seq = seq1 (#) seq2 iff for n holds seq.n =seq1.n * seq2.n proof thus seq = seq1 (#) seq2 implies for n holds seq.n =seq1.n * seq2.n proof assume A1: seq = seq1 (#) seq2; let n; dom seq = NAT by FUNCT_2:def 1; hence seq.n =seq1.n * seq2.n by A1,Def5; end; assume A2: for n holds seq.n =seq1.n * seq2.n; A3: dom seq = NAT /\ NAT by FUNCT_2:def 1 .= NAT /\ dom seq2 by FUNCT_2:def 1 .= dom seq1 /\ dom seq2 by FUNCT_2:def 1; for n st n in dom seq holds seq.n = seq1.n * seq2.n by A2; hence thesis by A3,Def5; end; definition let seq1,seq2; cluster seq1+seq2 -> total; coherence proof dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1; hence dom(seq1 + seq2) = NAT /\ NAT by Def3 .= NAT; end; cluster seq1(#)seq2 -> total; coherence proof dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1; hence dom(seq1 (#) seq2) = NAT /\ NAT by Def5 .= NAT; end; end; definition let C be set; let f be PartFunc of C,REAL; let r be real number; reconsider r1 = r as Element of REAL by XREAL_0:def 1; func r(#)f -> PartFunc of C,REAL means :Def6: dom it = dom f & for c being Element of C st c in dom it holds it.c = r * f.c; existence proof per cases; suppose A1: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f; deffunc U(Element of C') = r1 * f.$1; consider F be PartFunc of C',REAL such that A2: for c being Element of C' holds c in dom F iff X[c] and A3: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f by A2,SUBSET_1:8; thus thesis by A3; end; uniqueness proof deffunc U(Element of C) = r1 * f.$1; for f1, f2 be PartFunc of C,REAL st (dom f1 = dom f & for c being Element of C st c in dom f1 holds f1.c = U(c)) & (dom f2 = dom f & for c being Element of C st c in dom f2 holds f2.c = U(c)) holds f1 = f2 from UnPartFuncD'; hence thesis; end; end; definition let r,seq; cluster r(#)seq -> total; coherence proof thus dom(r(#)seq) = dom seq by Def6 .= NAT by FUNCT_2:def 1; end; end; theorem Th13: seq1 = r(#)seq2 iff for n holds seq1.n=r*seq2.n proof thus seq1 = r(#)seq2 implies for n holds seq1.n=r*seq2.n proof assume A1: seq1 = r(#)seq2; let n; dom(r(#)seq2) = NAT by FUNCT_2:def 1; hence thesis by A1,Def6; end; assume A2: for n holds seq1.n=r*seq2.n; A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1; for n st n in dom seq1 holds seq1.n = r * seq2.n by A2; hence thesis by A3,Def6; end; definition let C be set; let f be PartFunc of C,REAL; func -f ->PartFunc of C,REAL means :Def7: dom it = dom f & for c being Element of C st c in dom it holds it.c = -(f.c); existence proof per cases; suppose A1: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f; deffunc U(Element of C') = -(f.$1); consider F be PartFunc of C',REAL such that A2: for c being Element of C' holds c in dom F iff X[c] and A3: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f by A2,SUBSET_1:8; thus thesis by A3; end; uniqueness proof deffunc U(Element of C) = -(f.$1); for f1, f2 be PartFunc of C,REAL st (dom f1 = dom f & for c being Element of C st c in dom f1 holds f1.c = U(c)) & (dom f2 = dom f & for c being Element of C st c in dom f2 holds f2.c = U(c)) holds f1 = f2 from UnPartFuncD'; hence thesis; end; end; definition let seq; cluster - seq -> total; coherence proof thus dom -seq = dom seq by Def7 .= NAT by FUNCT_2:def 1; end; end; theorem Th14: seq1 = -seq2 iff for n holds seq1.n= -seq2.n proof thus seq1 = -seq2 implies for n holds seq1.n=-seq2.n proof assume A1: seq1 = -seq2; let n; dom(-seq2) = NAT by FUNCT_2:def 1; hence thesis by A1,Def7; end; assume A2: for n holds seq1.n= -seq2.n; A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1; for n st n in dom seq1 holds seq1.n = - seq2.n by A2; hence thesis by A3,Def7; end; definition let seq1,seq2; cluster seq1-seq2 -> total; coherence proof dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1; hence dom(seq1 - seq2) = NAT /\ NAT by Def4 .= NAT; end; end; theorem Th15: seq1 - seq2 = seq1 +- seq2 proof A1: dom(seq1 +- seq2) = NAT /\ NAT by FUNCT_2:def 1 .= NAT /\ dom seq2 by FUNCT_2:def 1 .= dom seq1 /\ dom seq2 by FUNCT_2:def 1; for c being Element of NAT st c in dom(seq1 +- seq2) holds (seq1 +- seq2).c = seq1.c - seq2.c proof let c be Element of NAT; assume c in dom(seq1 +- seq2); thus (seq1 +- seq2).c = seq1.c + (-seq2).c by Th11 .= seq1.c + -seq2.c by Th14 .= seq1.c - seq2.c by XCMPLX_0:def 8; end; hence thesis by A1,Def4; end; definition let seq; func seq" -> Real_Sequence means :Def8: for n holds it.n=(seq.n)"; existence proof deffunc U(Nat) = (seq.$1)"; thus ex f being Real_Sequence st for n holds f.n=U(n) from ExRealSeq; end; uniqueness proof let seq1,seq2 such that A1: for n holds seq1.n=(seq.n)" and A2: for n holds seq2.n=(seq.n)"; now let n; seq1.n=(seq.n)" & seq2.n=(seq.n)" by A1,A2; hence seq1.n=seq2.n; end; hence seq1=seq2 by FUNCT_2:113; end; end; definition let seq1,seq; func seq1 /" seq ->Real_Sequence equals :Def9: seq1(#)(seq"); correctness; end; definition let C be set; let f be PartFunc of C,REAL; func abs f -> PartFunc of C,REAL means :Def10: dom it = dom f & for c being Element of C st c in dom it holds it.c = abs(f.c); existence proof per cases; suppose A1: C is empty; reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56; take F; thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3; thus thesis by RELAT_1:60; suppose C is non empty; then reconsider C' = C as non empty set; defpred X[set] means $1 in dom f; deffunc U(Element of C') = abs(f.$1); consider F be PartFunc of C',REAL such that A2: for c being Element of C' holds c in dom F iff X[c] and A3: for c being Element of C' st c in dom F holds F.c = U(c) from LambdaPFD'; reconsider F as PartFunc of C,REAL; take F; thus dom F = dom f by A2,SUBSET_1:8; thus thesis by A3; end; uniqueness proof deffunc U(Element of C) = abs(f.$1); for f1, f2 be PartFunc of C,REAL st (dom f1 = dom f & for c being Element of C st c in dom f1 holds f1.c = U(c)) & (dom f2 = dom f & for c being Element of C st c in dom f2 holds f2.c = U(c)) holds f1 = f2 from UnPartFuncD'; hence thesis; end; end; definition let seq; cluster abs seq -> total; coherence proof thus dom abs seq = dom seq by Def10 .= NAT by FUNCT_2:def 1; end; end; theorem Th16: seq1 = abs seq iff for n holds seq1.n= abs(seq.n) proof thus seq1 = abs seq implies for n holds seq1.n=abs(seq.n) proof assume A1: seq1 = abs(seq); let n; dom(abs(seq)) = NAT by FUNCT_2:def 1; hence thesis by A1,Def10; end; assume A2: for n holds seq1.n= abs(seq.n); A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq by FUNCT_2:def 1; for n st n in dom seq1 holds seq1.n = abs(seq.n) by A2; hence thesis by A3,Def10; end; canceled 3; theorem Th20: (seq1+seq2)+seq3=seq1+(seq2+seq3) proof now let n; thus ((seq1+seq2)+seq3).n=(seq1+seq2).n+ seq3.n by Th11 .=seq1.n+seq2.n+seq3.n by Th11 .=seq1.n+(seq2.n+seq3.n) by XCMPLX_1:1 .=seq1.n+(seq2+seq3).n by Th11 .=(seq1+(seq2+seq3)).n by Th11; end; hence thesis by FUNCT_2:113; end; canceled; theorem Th22: (seq1(#)seq2)(#)seq3=seq1(#)(seq2(#)seq3) proof now let n; thus ((seq1(#)seq2)(#)seq3).n=(seq1(#)seq2).n*seq3.n by Th12 .=seq1.n*seq2.n*seq3.n by Th12 .=seq1.n*(seq2.n*seq3.n) by XCMPLX_1:4 .=seq1.n*(seq2(#)seq3).n by Th12 .=(seq1(#)(seq2(#)seq3)).n by Th12; end; hence thesis by FUNCT_2:113; end; theorem Th23: (seq1+seq2)(#)seq3=seq1(#)seq3+seq2(#)seq3 proof now let n; thus ((seq1+seq2)(#)seq3).n=(seq1+seq2).n*seq3.n by Th12 .=(seq1.n+seq2.n)*seq3.n by Th11 .=seq1.n*seq3.n+seq2.n*seq3.n by XCMPLX_1:8 .=(seq1(#)seq3).n+seq2.n*seq3.n by Th12 .=(seq1(#)seq3).n+(seq2(#)seq3).n by Th12 .=((seq1(#)seq3)+(seq2(#)seq3)).n by Th11; end; hence thesis by FUNCT_2:113; end; theorem seq3(#)(seq1+seq2)=seq3(#)seq1+seq3(#)seq2 by Th23; theorem Th25: -seq=(-1)(#)seq proof now let n; thus ((-1)(#)seq).n=(-1)*seq.n by Th13 .=-(1*seq.n) by XCMPLX_1:175 .=(-seq).n by Th14; end; hence thesis by FUNCT_2:113; end; theorem Th26: r(#)(seq1(#)seq2)=r(#)seq1(#)seq2 proof now let n; thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th13 .=r*(seq1.n*seq2.n) by Th12 .=(r*seq1.n)*seq2.n by XCMPLX_1:4 .=(r(#)seq1).n*seq2.n by Th13 .=(r(#)seq1 (#) seq2).n by Th12; end; hence thesis by FUNCT_2:113; end; theorem Th27: r(#)(seq1(#)seq2)=seq1(#)(r(#)seq2) proof now let n; thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th13 .=r*(seq1.n*seq2.n) by Th12 .=seq1.n*(r*seq2.n) by XCMPLX_1:4 .=seq1.n*(r(#)seq2).n by Th13 .=(seq1(#)(r(#)seq2)).n by Th12; end; hence thesis by FUNCT_2:113; end; theorem Th28: (seq1-seq2)(#)seq3=seq1(#)seq3-seq2(#)seq3 proof thus (seq1-seq2)(#)seq3=(seq1+-seq2)(#)seq3 by Th15 .=seq1(#)seq3+(-seq2)(#)seq3 by Th23 .=seq1(#)seq3+((-1)(#)seq2)(#)seq3 by Th25 .=seq1(#)seq3+(-1)(#)(seq2(#)seq3) by Th26 .=seq1(#)seq3+-(seq2(#)seq3) by Th25 .=seq1(#)seq3-seq2(#)seq3 by Th15; end; theorem seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2) by Th28; theorem Th30: r(#)(seq1+seq2)=r(#)seq1+r(#)seq2 proof now let n; thus (r(#)(seq1 + seq2)).n=r*(seq1+seq2).n by Th13 .=r*(seq1.n+seq2.n) by Th11 .=r*seq1.n+r*seq2.n by XCMPLX_1:8 .=(r(#)seq1).n+r*seq2.n by Th13 .=(r(#)seq1).n+(r(#)seq2).n by Th13 .=((r(#)seq1)+(r(#)seq2)).n by Th11; end; hence thesis by FUNCT_2:113; end; theorem Th31: (r*p)(#)seq=r(#)(p(#)seq) proof now let n; thus ((r*p)(#)seq).n=(r*p)*seq.n by Th13 .=r*(p*seq.n) by XCMPLX_1:4 .=r*(p(#)seq).n by Th13 .=(r(#)(p(#)seq)).n by Th13; end; hence thesis by FUNCT_2:113; end; theorem Th32: r(#)(seq1-seq2)=r(#)seq1-r(#)seq2 proof thus r(#)(seq1-seq2)=r(#)(seq1+-seq2) by Th15 .=r(#)seq1+r(#)(-seq2) by Th30 .=r(#)seq1+r(#)((-1)(#)seq2) by Th25 .=r(#)seq1+((-1)*r)(#)seq2 by Th31 .=r(#)seq1+(-1)(#)(r(#)seq2) by Th31 .=r(#)seq1+-(r(#)seq2) by Th25 .=r(#)seq1-(r(#)seq2) by Th15; end; theorem Th33: r(#)(seq1/"seq)=(r(#)seq1)/"seq proof thus r(#)(seq1/"seq)=r(#)(seq1(#)seq") by Def9 .=(r(#)seq1)(#)(seq") by Th26 .=(r(#)seq1)/"seq by Def9; end; theorem seq1-(seq2+seq3)=seq1-seq2-seq3 proof thus seq1-(seq2+seq3)=seq1+-(seq2+seq3) by Th15 .=seq1+(-1)(#)(seq2+seq3) by Th25 .=seq1+((-1)(#)seq2+(-1)(#)seq3) by Th30 .=seq1+(-seq2+(-1)(#)seq3) by Th25 .=seq1+(-seq2+-seq3) by Th25 .=seq1+-seq2+-seq3 by Th20 .=seq1-seq2+-seq3 by Th15 .=seq1-seq2-seq3 by Th15; end; theorem Th35: 1(#)seq=seq proof now let n; thus (1(#)seq).n=1*seq.n by Th13 .=seq.n; end; hence thesis by FUNCT_2:113; end; theorem Th36: -(-seq)=seq proof thus -(-seq)=(-1)(#)(-seq) by Th25 .=(-1)(#)((-1)(#)seq) by Th25 .=((-1)*(-1))(#)seq by Th31 .=seq by Th35; end; theorem Th37: seq1-(-seq2)=seq1+seq2 proof thus seq1-(-seq2)=seq1+(-(-seq2)) by Th15 .=seq1+seq2 by Th36; end; theorem seq1-(seq2-seq3)=seq1-seq2+seq3 proof thus seq1-(seq2-seq3)=seq1+-(seq2-seq3) by Th15 .=seq1+(-1)(#)(seq2-seq3) by Th25 .=seq1+((-1)(#)seq2-((-1)(#)seq3)) by Th32 .=seq1+(-seq2-((-1)(#)seq3)) by Th25 .=seq1+(-seq2-(-seq3)) by Th25 .=seq1+(-seq2+seq3) by Th37 .=seq1+-seq2+seq3 by Th20 .=seq1-seq2+seq3 by Th15; end; theorem seq1+(seq2-seq3)=seq1+seq2-seq3 proof thus seq1+(seq2-seq3)=seq1+(seq2+-seq3) by Th15 .=seq1+seq2+-seq3 by Th20 .=seq1+seq2-seq3 by Th15; end; theorem (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2) proof thus (-seq1)(#)seq2=(-1)(#)seq1(#)seq2 by Th25 .=(-1)(#)(seq1(#)seq2) by Th26 .=-(seq1(#)seq2) by Th25; thus seq1(#)(-seq2)=seq1(#)((-1)(#)seq2) by Th25 .=(-1)(#)(seq1(#)seq2) by Th27 .=-(seq1(#)seq2) by Th25; end; theorem Th41:seq is being_not_0 implies seq" is being_not_0 proof assume that A1: seq is being_not_0 and A2: not seq" is being_not_0; consider n1 such that A3: (seq").n1=0 by A2,Th7; A4: seq.n1<>0 by A1,Th7; (seq.n1)"=(seq").n1 by Def8; hence contradiction by A3,A4,XCMPLX_1:203; end; theorem Th42:seq""=seq proof now let n; thus (seq"").n=((seq").n)" by Def8 .=(seq.n)"" by Def8 .=seq.n; end; hence thesis by FUNCT_2:113; end; theorem Th43:seq is being_not_0 & seq1 is being_not_0 iff seq(#)seq1 is being_not_0 proof thus seq is being_not_0 & seq1 is being_not_0 implies seq(#)seq1 is being_not_0 proof assume that A1: seq is being_not_0 and A2: seq1 is being_not_0; now let n; A3: seq.n<>0 by A1,Th7; A4: seq1.n<>0 by A2,Th7; (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12; hence (seq(#)seq1).n<>0 by A3,A4,XCMPLX_1:6; end; hence thesis by Th7; end; assume A5: seq(#)seq1 is being_not_0; now let n; (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12; hence seq.n<>0 by A5,Th7; end; hence seq is being_not_0 by Th7; now let n; (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12; hence seq1.n<>0 by A5,Th7; end; hence seq1 is being_not_0 by Th7; end; theorem Th44:seq"(#)seq1"=(seq(#)seq1)" proof now let n; thus ((seq")(#)(seq1")).n=((seq").n)*((seq1").n) by Th12 .=((seq").n)*(seq1.n)" by Def8 .=(seq.n)"*(seq1.n)" by Def8 .=((seq.n)*(seq1.n))" by XCMPLX_1:205 .=((seq(#)seq1).n)" by Th12 .=((seq(#)seq1)").n by Def8; end; hence thesis by FUNCT_2:113; end; theorem seq is being_not_0 implies (seq1/"seq)(#)seq=seq1 proof assume A1: seq is being_not_0; now let n; A2: seq.n<>0 by A1,Th7; thus ((seq1/"seq)(#)seq).n=((seq1/"seq).n)*seq.n by Th12 .=((seq1(#)seq").n)*seq.n by Def9 .=(seq1.n)*(seq".n)*seq.n by Th12 .=(seq1.n)*(seq.n)"*seq.n by Def8 .=(seq1.n)*((seq.n)"*seq.n) by XCMPLX_1:4 .=(seq1.n)*1 by A2,XCMPLX_0:def 7 .=seq1.n; end; hence thesis by FUNCT_2:113; end; theorem (seq'/"seq)(#)(seq1'/"seq1)=(seq'(#)seq1')/"(seq(#)seq1) proof now let n; thus ((seq'/"seq)(#)(seq1'/"seq1)).n=((seq'/"seq).n)*(seq1'/"seq1).n by Th12 .=((seq'(#)seq").n)*(seq1'/"seq1).n by Def9 .=((seq'(#)seq").n)*(seq1'(#)seq1").n by Def9 .=(seq'.n)*(seq".n)*(seq1'(#)seq1").n by Th12 .=(seq'.n)*(seq".n)*((seq1'.n)*seq1".n) by Th12 .=(seq'.n)*(seq".n)*(seq1'.n)*seq1".n by XCMPLX_1:4 .=(seq'.n)*((seq1'.n)*(seq".n))*seq1".n by XCMPLX_1:4 .=(seq'.n)*(((seq1'.n)*(seq".n))*seq1".n) by XCMPLX_1:4 .=(seq'.n)*((seq1'.n)*((seq".n)*seq1".n)) by XCMPLX_1:4 .=(seq'.n)*((seq1'.n)*((seq"(#)seq1").n)) by Th12 .=(seq'.n)*(seq1'.n)*((seq"(#)seq1").n) by XCMPLX_1:4 .=(seq'.n)*(seq1'.n)*((seq(#)seq1)".n) by Th44 .=((seq'(#)seq1').n)*(seq(#)seq1)".n by Th12 .=((seq'(#)seq1')(#)(seq(#)seq1)").n by Th12 .=((seq'(#)seq1')/"(seq(#)seq1)).n by Def9; end; hence thesis by FUNCT_2:113; end; theorem seq is being_not_0 & seq1 is being_not_0 implies seq/"seq1 is being_not_0 proof assume that A1: seq is being_not_0 and A2: seq1 is being_not_0; seq1" is being_not_0 by A2,Th41; then seq(#)seq1" is being_not_0 by A1,Th43; hence thesis by Def9; end; theorem Th48:(seq/"seq1)"=seq1/"seq proof now let n; thus (seq/"seq1)".n=(seq(#)seq1")".n by Def9 .=(seq"(#)seq1"").n by Th44 .=(seq1(#)seq").n by Th42 .=(seq1/"seq).n by Def9; end; hence thesis by FUNCT_2:113; end; theorem Th49: seq2(#)(seq1/"seq)=(seq2(#)seq1)/"seq proof now let n; thus (seq2(#)(seq1/"seq)).n=(seq2(#)(seq1(#)seq")).n by Def9 .=(seq2(#)seq1(#)seq").n by Th22 .=((seq2(#)seq1)/"seq).n by Def9; end; hence thesis by FUNCT_2:113; end; theorem seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq proof now let n; thus (seq2/"(seq/"seq1)).n=((seq2(#)(seq/"seq1)")).n by Def9 .=((seq2(#)(seq1/"seq))).n by Th48 .=((seq2(#)seq1)/"seq).n by Th49; end; hence thesis by FUNCT_2:113; end; theorem Th51:seq1 is being_not_0 implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1) proof assume that A1: seq1 is being_not_0; now let n; A2: seq1.n<>0 by A1,Th7; thus (seq2/"seq).n=(seq2(#)seq").n by Def9 .=(seq2.n)*1*seq".n by Th12 .=(seq2.n)*((seq1.n)*(seq1.n)")*seq".n by A2,XCMPLX_0:def 7 .=(seq2.n)*(((seq1.n)*(seq1.n)")*seq".n) by XCMPLX_1:4 .=(seq2.n)*((seq1.n)*((seq1.n)"*seq".n)) by XCMPLX_1:4 .=(seq2.n)*(seq1.n)*((seq1.n)"*seq".n) by XCMPLX_1:4 .=((seq2(#)seq1).n)*((seq1.n)"*seq".n) by Th12 .=((seq2(#)seq1).n)*((seq1".n)*seq".n) by Def8 .=((seq2(#)seq1).n)*(seq"(#)seq1").n by Th12 .=((seq2(#)seq1).n)*(seq(#)seq1)".n by Th44 .=((seq2(#)seq1)(#)(seq(#)seq1)").n by Th12 .=((seq2(#)seq1)/"(seq(#)seq1)).n by Def9; end; hence thesis by FUNCT_2:113; end; theorem Th52:r<>0 & seq is being_not_0 implies r(#)seq is being_not_0 proof assume that A1: r<>0 and A2: seq is being_not_0 and A3: not r(#)seq is being_not_0; consider n1 such that A4: (r(#)seq).n1=0 by A3,Th7; A5: r*seq.n1=0 by A4,Th13; seq.n1 <> 0 by A2,Th7; hence contradiction by A1,A5,XCMPLX_1:6; end; theorem seq is being_not_0 implies -seq is being_not_0 proof assume seq is being_not_0; then (-1)(#)seq is being_not_0 by Th52; hence thesis by Th25; end; theorem Th54:(r(#)seq)"=r"(#)seq" proof now let n; thus (r(#)seq)".n=((r(#)seq).n)" by Def8 .=(r*(seq.n))" by Th13 .=r"*(seq.n)" by XCMPLX_1:205 .=r"*seq".n by Def8 .=(r"(#)seq").n by Th13; end; hence thesis by FUNCT_2:113; end; Lm1:(-1)"=-1; theorem Th55:(-seq)"=(-1)(#)seq" proof thus (-seq)"=((-1)(#)seq)" by Th25 .=(-1)(#)seq" by Lm1,Th54; end; theorem -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/"seq proof thus -seq1/"seq=(-1)(#)(seq1/"seq) by Th25 .=((-1)(#)seq1)/"seq by Th33 .=(-seq1)/"seq by Th25; thus seq1/"(-seq)=seq1(#)(-seq)" by Def9 .=seq1(#)((-1)(#)seq") by Th55 .=(-1)(#)(seq1(#)(seq")) by Th27 .=-(seq1(#)seq") by Th25 .=-(seq1/"seq) by Def9; end; theorem Th57: seq1/"seq + seq1'/"seq=(seq1+seq1')/"seq & seq1/"seq - seq1'/"seq=(seq1-seq1')/"seq proof thus seq1/"seq+seq1'/"seq=seq1(#)seq" +seq1'/"seq by Def9 .=seq1(#)seq" +seq1'(#)seq" by Def9 .=(seq1+seq1')(#)seq" by Th23 .=(seq1+seq1')/"seq by Def9; thus seq1/"seq-seq1'/"seq=seq1(#)seq" -seq1'/"seq by Def9 .=seq1(#)seq" -seq1'(#)seq" by Def9 .=(seq1-seq1')(#)seq" by Th28 .=(seq1-seq1')/"seq by Def9; end; theorem seq is being_not_0 & seq' is being_not_0 implies (seq1/"seq + seq1'/"seq'=(seq1(#)seq'+seq1'(#)seq)/"(seq(#)seq')) & (seq1/"seq - seq1'/"seq'=(seq1(#)seq'-seq1'(#)seq)/"(seq(#)seq')) proof assume that A1: seq is being_not_0 and A2: seq' is being_not_0; thus seq1/"seq + seq1'/"seq'=(seq1(#)seq')/"(seq(#)seq')+seq1'/"seq' by A2,Th51 .=(seq1(#)seq')/"(seq(#)seq')+(seq1'(#)seq)/"(seq(#)seq') by A1,Th51 .=(seq1(#)seq'+seq1'(#)seq)/"(seq(#)seq') by Th57; thus seq1/"seq - seq1'/"seq'=(seq1(#)seq')/"(seq(#)seq')-seq1'/"seq' by A2,Th51 .=(seq1(#)seq')/"(seq(#)seq')-(seq1'(#)seq)/"(seq(#)seq') by A1,Th51 .=(seq1(#)seq'-seq1'(#)seq)/"(seq(#)seq') by Th57; end; theorem (seq1'/"seq)/"(seq'/"seq1)=(seq1'(#)seq1)/"(seq(#)seq') proof thus (seq1'/"seq)/"(seq'/"seq1)=(seq1'/"seq)(#)(seq'/"seq1)" by Def9 .=(seq1'/"seq)(#)(seq'(#)seq1")" by Def9 .=(seq1'/"seq)(#)(seq'"(#)seq1"") by Th44 .=(seq1'/"seq)(#)(seq1(#)seq'") by Th42 .=(seq1'(#)seq")(#)(seq1(#)seq'") by Def9 .=seq1'(#)seq"(#)seq1(#)seq'" by Th22 .=seq1'(#)(seq1(#)seq")(#)seq'" by Th22 .=seq1'(#)((seq1(#)seq")(#)seq'") by Th22 .=seq1'(#)(seq1(#)(seq"(#)seq'")) by Th22 .=seq1'(#)seq1(#)(seq"(#)seq'") by Th22 .=seq1'(#)seq1(#)(seq(#)seq')" by Th44 .=(seq1'(#)seq1)/"(seq(#)seq') by Def9; end; theorem Th60:abs(seq(#)seq')=abs(seq)(#)abs(seq') proof now let n; thus (abs(seq(#)seq')).n=abs(((seq(#)seq').n)) by Th16 .=abs((seq.n)*(seq'.n)) by Th12 .=abs((seq.n))*abs((seq'.n)) by ABSVALUE:10 .=((abs(seq)).n)*abs((seq'.n)) by Th16 .=((abs(seq)).n)*(abs(seq')).n by Th16 .=(abs(seq)(#)abs(seq')).n by Th12; end; hence thesis by FUNCT_2:113; end; theorem seq is being_not_0 implies abs(seq) is being_not_0 proof assume A1: seq is being_not_0; now let n; seq.n<>0 by A1,Th7; then abs(seq.n)<>0 by ABSVALUE:6; hence (abs(seq)).n<>0 by Th16; end; hence thesis by Th7; end; theorem Th62:abs(seq)"=abs(seq") proof now let n; thus (abs(seq")).n=abs(seq".n) by Th16 .=abs((seq.n)") by Def8 .=abs(1/(seq.n)) by XCMPLX_1:217 .=1/abs(seq.n) by ABSVALUE:15 .=(abs(seq.n))" by XCMPLX_1:217 .=(abs(seq).n)" by Th16 .=(abs(seq))".n by Def8; end; hence thesis by FUNCT_2:113; end; theorem abs(seq'/"seq)=abs(seq')/"abs(seq) proof thus abs(seq'/"seq)=abs(seq'(#)seq") by Def9 .=abs(seq')(#)abs(seq") by Th60 .=abs(seq')(#)abs(seq)" by Th62 .=abs(seq')/"abs(seq) by Def9; end; theorem abs(r(#)seq)=abs(r)(#)abs(seq) proof now let n; thus abs(r(#)seq).n=abs((r(#)seq).n) by Th16 .=abs(r*(seq.n)) by Th13 .=abs(r)*abs(seq.n) by ABSVALUE:10 .=abs(r)*(abs(seq)).n by Th16 .=(abs(r)(#)abs(seq)).n by Th13; end; hence thesis by FUNCT_2:113; end;