### The Mizar article:

### Partial Functions from a Domain to the Set of Real Numbers

**by****Jaroslaw Kotowicz**

- Received May 27, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: RFUNCT_1
- [ MML identifier index ]

environ vocabulary PARTFUN1, ARYTM, ARYTM_1, RELAT_1, ARYTM_3, BOOLE, FUNCT_1, FINSEQ_1, SEQ_1, ABSVALUE, FUNCT_3, PARTFUN2, RFUNCT_1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, FUNCT_3, ABSVALUE, RELSET_1, PARTFUN1, PARTFUN2, SEQ_1; constructors REAL_1, FUNCT_3, ABSVALUE, PARTFUN1, PARTFUN2, SEQ_1, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, PARTFUN1, XBOOLE_0; theorems TARSKI, AXIOMS, SUBSET_1, FUNCT_1, FUNCT_3, REAL_1, ABSVALUE, PARTFUN1, PARTFUN2, RELSET_1, SEQ_1, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes SEQ_1; begin reserve x,X,Y for set; reserve C for non empty set; reserve c for Element of C; reserve f,f1,f2,f3,g,g1 for PartFunc of C,REAL; reserve r,r1,r2,p,p1 for real number; Lm1: (-1)"=-1; canceled; theorem Th2: 0<=p & 0<=r & p<=p1 & r<=r1 implies p*r<=p1*r1 proof assume A1: 0<=p & 0<=r & p<=p1 & r<=r1; then A2: p*r1<=p1*r1 by AXIOMS:25; p*r<=p*r1 by A1,AXIOMS:25; hence thesis by A2,AXIOMS:22; end; :: ::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS :: definition let C;let f1,f2; canceled 3; func f1/f2 -> PartFunc of C,REAL means :Def4: dom it = dom f1 /\ (dom f2 \ f2"{0}) & for c st c in dom it holds it.c = f1.c * (f2.c)"; existence proof defpred P[set] means $1 in dom f1 /\ (dom f2 \ f2"{0}); deffunc G(set)=f1.$1 * (f2.$1)"; consider F being PartFunc of C,REAL such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F.c = G(c) from LambdaPFD'; take F; thus dom F = dom f1 /\ (dom f2 \ f2"{0}) by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof deffunc F(set)=f1.$1 * (f2.$1)"; for f,g being PartFunc of C,REAL st (dom f=dom f1 /\ (dom f2 \ f2"{0}) & for c be Element of C st c in dom f holds f.c = F(c)) & (dom g=dom f1 /\ (dom f2 \ f2"{0}) & for c be Element of C st c in dom g holds g.c = F(c)) holds f = g from UnPartFuncD'; hence thesis; end; end; definition let C; let f; canceled 3; func f^ -> PartFunc of C,REAL means :Def8: dom it = dom f \ f"{0} & for c st c in dom it holds it.c = (f.c)"; existence proof defpred P[set] means $1 in dom f \ f"{0}; deffunc H(set)=(f.$1)"; consider F being PartFunc of C,REAL such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F.c = H(c) from LambdaPFD'; take F; thus dom F = dom f \ f"{0} by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof deffunc H(Element of C)=(f.$1)"; for f1,g being PartFunc of C,REAL st ( dom f1= (dom f \ f"{0}) & for c be Element of C st c in dom f1 holds f1.c = H(c) ) & (dom g= (dom f \ f"{0}) & for c be Element of C st c in dom g holds g.c = H(c)) holds f1 = g from UnPartFuncD'; hence thesis; end; end; canceled 8; theorem Th11: dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0} proof dom (g^) = dom g \ g"{0} by Def8; hence dom (g^) c= dom g by XBOOLE_1:36; dom g \ g"{0} c= dom g by XBOOLE_1:36; hence thesis by XBOOLE_1:28; end; theorem Th12: dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) proof thus dom (f1(#)f2) \ (f1(#)f2)"{0} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) proof let x; assume A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0}; then A2: x in dom (f1(#)f2) & not x in (f1(#)f2)"{0} by XBOOLE_0:def 4; reconsider x1=x as Element of C by A1; not (f1(#)f2).x1 in {0} by A2,FUNCT_1:def 13; then (f1(#)f2).x1 <> 0 by TARSKI:def 1; then f1.x1 * f2.x1 <> 0 by A2,SEQ_1:def 5; then f1.x1 <> 0 & f2.x1 <> 0; then x1 in dom f1 /\ dom f2 & not f1.x1 in {0} & not f2.x1 in {0} by A2,SEQ_1:def 5,TARSKI:def 1; then x1 in dom f1 & x1 in dom f2 & not x1 in (f1)"{0} & not f2.x1 in {0} by FUNCT_1:def 13,XBOOLE_0:def 3; then x in dom f1 \ (f1)"{0} & x1 in dom f2 & not x1 in (f2)"{0} by FUNCT_1:def 13,XBOOLE_0:def 4; then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0} by XBOOLE_0:def 4; hence x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) by XBOOLE_0:def 3; end; thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) c= dom (f1(#)f2) \ (f1(#)f2)"{0} proof let x; assume A3: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}); then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0} by XBOOLE_0:def 3; then A4: x in dom f1 & not x in (f1)"{0} & x in dom f2 & not x in (f2)"{0} by XBOOLE_0:def 4; reconsider x1=x as Element of C by A3; not f1.x1 in {0} by A4,FUNCT_1:def 13; then A5: f1.x1 <> 0 by TARSKI:def 1; not f2.x1 in {0} by A4,FUNCT_1:def 13; then f2.x1 <> 0 by TARSKI:def 1; then A6: f1.x1 * f2.x1 <>0 by A5,XCMPLX_1:6; x1 in dom f1 /\ dom f2 by A4,XBOOLE_0:def 3; then A7: x1 in dom (f1(#)f2) by SEQ_1:def 5; then (f1(#)f2).x1 <> 0 by A6,SEQ_1:def 5; then not (f1(#)f2).x1 in {0} by TARSKI:def 1; then not x in (f1(#)f2)"{0} by FUNCT_1:def 13; hence x in dom (f1(#)f2) \ (f1(#)f2)"{0}by A7,XBOOLE_0:def 4; end; end; theorem Th13: c in dom (f^) implies f.c <> 0 proof assume that A1: c in dom (f^) and A2: f.c = 0; A3: c in dom f \ f"{0} by A1,Def8; then A4: c in dom f & not c in f"{0} by XBOOLE_0:def 4; now per cases by A4,FUNCT_1:def 13; suppose not c in dom f; hence contradiction by A3,XBOOLE_0:def 4; suppose not f.c in {0}; hence contradiction by A2,TARSKI:def 1; end; hence contradiction; end; theorem Th14: (f^)"{0} = {} proof assume A1: (f^)"{0} <> {}; consider x being Element of (f^)"{0}; A2: x in dom (f^) & ((f^) qua Function).x in {0} by A1,FUNCT_1:def 13; then reconsider x as Element of C; (f^).x = 0 by A2,TARSKI:def 1; then A3: (f.x)" = 0 by A2,Def8; x in dom f \ f"{0} by A2,Def8; then x in dom f & not x in f"{0} by XBOOLE_0:def 4; then not f.x in {0} by FUNCT_1:def 13; then f.x <> 0 by TARSKI:def 1; hence contradiction by A3,XCMPLX_1:203; end; theorem Th15: (abs(f))"{0} = f"{0} & (-f)"{0} = f"{0} proof now let c; thus c in (abs(f))"{0} implies c in f"{0} proof assume c in (abs(f))"{0}; then c in dom (abs(f)) & (abs(f)).c in {0} by FUNCT_1:def 13; then c in dom (abs(f)) & (abs(f)).c = 0 by TARSKI:def 1; then c in dom (abs(f)) & abs(f.c) = 0 by SEQ_1:def 10; then c in dom f & f.c = 0 by ABSVALUE:7,SEQ_1:def 10; then c in dom f & f.c in {0} by TARSKI:def 1; hence thesis by FUNCT_1:def 13; end; assume c in (f)"{0}; then c in dom f & f.c in {0} by FUNCT_1:def 13; then c in dom (abs(f)) & f.c = 0 by SEQ_1:def 10,TARSKI:def 1; then c in dom (abs(f)) & abs(f.c) = 0 by ABSVALUE:7; then c in dom (abs(f)) & (abs(f)).c = 0 by SEQ_1:def 10; then c in dom (abs(f)) & (abs(f)).c in {0} by TARSKI:def 1; hence c in (abs(f))"{0} by FUNCT_1:def 13; end; hence (abs(f))"{0} = f"{0} by SUBSET_1:8; now let c; thus c in (-f)"{0} implies c in f"{0} proof assume c in (-f)"{0}; then c in dom (-f) & (-f).c in {0} by FUNCT_1:def 13; then c in dom (-f) & (-f).c = 0 by TARSKI:def 1; then c in dom (-f) & --(f.c) = -0 by SEQ_1:def 7; then c in dom f & f.c in {0} by SEQ_1:def 7,TARSKI:def 1; hence thesis by FUNCT_1:def 13; end; assume c in (f)"{0}; then c in dom f & f.c in {0} by FUNCT_1:def 13; then c in dom (-f) & f.c = 0 by SEQ_1:def 7,TARSKI:def 1; then c in dom (-f) & (-f).c = 0 by REAL_1:26,SEQ_1:def 7; then c in dom (-f) & (-f).c in {0} by TARSKI:def 1; hence c in (-f)"{0} by FUNCT_1:def 13; end; hence thesis by SUBSET_1:8; end; theorem Th16: dom (f^^) = dom (f|(dom (f^))) proof dom (f^) = dom f \ f"{0} by Def8; then A1: dom (f^) c= dom f by XBOOLE_1:36; thus dom (f^^) = dom (f^) \(f^)"{0} by Def8 .= dom (f^) \ {} by Th14 .= dom f /\ dom (f^) by A1,XBOOLE_1:28 .= dom (f|(dom (f^))) by RELAT_1:90; end; theorem Th17: r<>0 implies (r(#)f)"{0} = f"{0} proof assume A1: r<>0; now let c; thus c in (r(#)f)"{0} implies c in f"{0} proof assume c in (r(#)f)"{0}; then c in dom (r(#)f) & (r(#)f).c in {0} by FUNCT_1:def 13; then c in dom (r(#)f) & (r(#)f).c = 0 by TARSKI:def 1; then c in dom (r(#)f) & r*f.c = 0 by SEQ_1:def 6; then c in dom f & f.c = 0 by A1,SEQ_1:def 6,XCMPLX_1:6; then c in dom f & f.c in {0} by TARSKI:def 1; hence thesis by FUNCT_1:def 13; end; assume c in (f)"{0}; then c in dom f & f.c in {0} by FUNCT_1:def 13; then c in dom f & f.c = 0 by TARSKI:def 1; then c in dom (r(#)f) & r*f.c = 0 by SEQ_1:def 6; then c in dom (r(#)f) & (r(#)f).c = 0 by SEQ_1:def 6; then c in dom (r(#)f) & (r(#)f).c in {0} by TARSKI:def 1; hence c in (r(#)f)"{0} by FUNCT_1:def 13; end; hence thesis by SUBSET_1:8; end; :: :: BASIC PROPERTIES OF OPERATIONS :: canceled; theorem (f1 + f2) + f3 = f1 + (f2 + f3) proof A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by SEQ_1:def 3 .= dom f1 /\ dom f2 /\ dom f3 by SEQ_1:def 3 .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom f1 /\ dom (f2 + f3) by SEQ_1:def 3 .= dom (f1 + (f2 + f3)) by SEQ_1:def 3; now let c; assume A2: c in dom (f1 + f2 + f3); then c in dom f1 /\ dom (f2 + f3) by A1,SEQ_1:def 3; then A3: c in dom (f2 + f3) by XBOOLE_0:def 3; c in dom (f1 + f2) /\ dom f3 by A2,SEQ_1:def 3; then A4: c in dom (f1 + f2) by XBOOLE_0:def 3; thus (f1 + f2 + f3).c = (f1 + f2).c + f3.c by A2,SEQ_1:def 3 .= f1.c + f2.c + f3.c by A4,SEQ_1:def 3 .= f1.c + (f2.c + f3.c) by XCMPLX_1:1 .= f1.c + (f2 + f3).c by A3,SEQ_1:def 3 .= (f1 + (f2 + f3)).c by A1,A2,SEQ_1:def 3; end; hence thesis by A1,PARTFUN1:34; end; canceled; theorem Th21: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by SEQ_1:def 5 .= dom f1 /\ dom f2 /\ dom f3 by SEQ_1:def 5 .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom f1 /\ dom (f2 (#) f3) by SEQ_1:def 5 .= dom (f1 (#) (f2 (#) f3)) by SEQ_1:def 5; now let c; assume A2: c in dom (f1(#)f2(#)f3); then c in dom f1 /\ dom (f2(#)f3) by A1,SEQ_1:def 5; then A3: c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 (#) f2) /\ dom f3 by A2,SEQ_1:def 5; then A4: c in dom (f1 (#) f2) by XBOOLE_0:def 3; thus (f1 (#) f2 (#) f3).c = (f1 (#) f2).c * f3.c by A2,SEQ_1:def 5 .= f1.c * f2.c * f3.c by A4,SEQ_1:def 5 .= f1.c * (f2.c * f3.c) by XCMPLX_1:4 .= f1.c * (f2 (#) f3).c by A3,SEQ_1:def 5 .= (f1 (#) (f2 (#) f3)).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem Th22: (f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3 proof A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by SEQ_1:def 5 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 3 .= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by SEQ_1:def 5 .= dom (f1 (#) f3) /\ dom (f2 (#) f3) by SEQ_1:def 5 .= dom (f1 (#) f3 + f2 (#) f3) by SEQ_1:def 3; now let c; assume A2: c in dom ((f1 + f2)(#)f3); then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,SEQ_1:def 3; then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 + f2) /\ dom f3 by A2,SEQ_1:def 5; then A4: c in dom (f1 + f2) by XBOOLE_0:def 3; thus ((f1 + f2) (#) f3).c = (f1 + f2).c * f3.c by A2,SEQ_1:def 5 .= (f1.c + f2.c) * f3.c by A4,SEQ_1:def 3 .= f1.c * f3.c + f2.c * f3.c by XCMPLX_1:8 .= (f1 (#) f3).c + f2.c* f3.c by A3,SEQ_1:def 5 .= (f1 (#) f3).c + (f2 (#) f3).c by A3,SEQ_1:def 5 .=((f1 (#) f3) + (f2 (#) f3)).c by A1,A2,SEQ_1:def 3; end; hence thesis by A1,PARTFUN1:34; end; theorem f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2 by Th22; theorem Th24: r(#)(f1(#)f2)=r(#)f1(#)f2 proof A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 6 .= dom f1 /\ dom f2 by SEQ_1:def 5 .= dom (r(#)f1) /\ dom f2 by SEQ_1:def 6 .= dom (r(#)f1(#)f2) by SEQ_1:def 5; now let c; assume A2: c in dom (r(#)(f1(#)f2)); then c in dom (r(#)f1) /\ dom f2 by A1,SEQ_1:def 5; then A3: c in dom (r(#)f1) & c in dom f2 by XBOOLE_0:def 3; A4: c in dom (f1(#)f2) by A2,SEQ_1:def 6; thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,SEQ_1:def 6 .= r*(f1.c * f2.c) by A4,SEQ_1:def 5 .= (r*f1.c) * f2.c by XCMPLX_1:4 .= (r(#)f1).c * f2.c by A3,SEQ_1:def 6 .= (r(#)f1 (#) f2).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem Th25: r(#)(f1(#)f2)=f1(#)(r(#)f2) proof A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 6 .= dom f1 /\ dom f2 by SEQ_1:def 5 .= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6 .= dom (f1(#)(r(#)f2)) by SEQ_1:def 5; now let c; assume A2: c in dom (r(#)(f1(#)f2)); then c in dom f1 /\ dom (r(#)f2) by A1,SEQ_1:def 5; then A3: c in dom f1 & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1(#)f2) by A2,SEQ_1:def 6; thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,SEQ_1:def 6 .= r * (f1.c * f2.c) by A4,SEQ_1:def 5 .= f1.c * (r * f2.c) by XCMPLX_1:4 .= f1.c * (r(#)f2).c by A3,SEQ_1:def 6 .= (f1(#)(r(#)f2)).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem Th26: (f1 - f2)(#)f3=f1(#)f3 - f2(#)f3 proof A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by SEQ_1:def 5 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 4 .= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by SEQ_1:def 5 .= dom (f1 (#) f3) /\ dom (f2 (#) f3) by SEQ_1:def 5 .= dom (f1 (#) f3 - f2 (#) f3) by SEQ_1:def 4; now let c; assume A2: c in dom ((f1 - f2)(#)f3); then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,SEQ_1:def 4; then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 - f2) /\ dom f3 by A2,SEQ_1:def 5; then A4: c in dom (f1 - f2) by XBOOLE_0:def 3; thus ((f1 - f2) (#) f3).c = (f1 - f2).c * f3.c by A2,SEQ_1:def 5 .= (f1.c - f2.c) * f3.c by A4,SEQ_1:def 4 .= f1.c * f3.c - f2.c * f3.c by XCMPLX_1:40 .= (f1 (#) f3).c - f2.c * f3.c by A3,SEQ_1:def 5 .= (f1 (#) f3).c - (f2 (#) f3).c by A3,SEQ_1:def 5 .=((f1 (#) f3) - (f2 (#) f3)).c by A1,A2,SEQ_1:def 4; end; hence thesis by A1,PARTFUN1:34; end; theorem f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) by Th26; theorem r(#)(f1 + f2) = r(#)f1 + r(#)f2 proof A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by SEQ_1:def 6 .= dom f1 /\ dom f2 by SEQ_1:def 3 .= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6 .= dom (r(#)f1) /\ dom (r(#)f2) by SEQ_1:def 6 .= dom (r(#)f1 + r(#)f2) by SEQ_1:def 3; now let c; assume A2: c in dom (r(#)(f1 + f2)); then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,SEQ_1:def 3; then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1 + f2) by A2,SEQ_1:def 6; thus (r(#)(f1 + f2)).c = r * (f1 + f2).c by A2,SEQ_1:def 6 .= r * (f1.c + f2.c) by A4,SEQ_1:def 3 .= r * f1.c + r * f2.c by XCMPLX_1:8 .= (r(#)f1).c + r * f2.c by A3,SEQ_1:def 6 .= (r(#)f1).c + (r(#)f2).c by A3,SEQ_1:def 6 .= (r(#)f1 + r(#)f2).c by A1,A2,SEQ_1:def 3; end; hence thesis by A1,PARTFUN1:34; end; theorem Th29: (r*p)(#)f = r(#)(p(#)f) proof A1: dom ((r*p) (#) f) = dom f by SEQ_1:def 6 .= dom (p(#)f) by SEQ_1:def 6 .= dom (r(#)(p(#)f)) by SEQ_1:def 6; now let c; assume A2: c in dom ((r*p)(#)f); then A3: c in dom (p(#)f) by A1,SEQ_1:def 6; thus ((r*p)(#)f).c = r*p * f.c by A2,SEQ_1:def 6 .= r*(p * f.c) by XCMPLX_1:4 .= r * (p(#)f).c by A3,SEQ_1:def 6 .= (r(#)(p(#)f)).c by A1,A2,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem r(#)(f1 - f2) = r(#)f1 - r(#)f2 proof A1: dom (r(#)(f1 - f2)) = dom (f1 - f2) by SEQ_1:def 6 .= dom f1 /\ dom f2 by SEQ_1:def 4 .= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6 .= dom (r(#)f1) /\ dom (r(#)f2) by SEQ_1:def 6 .= dom (r(#)f1 - r(#)f2) by SEQ_1:def 4; now let c; assume A2: c in dom (r(#)(f1 - f2)); then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,SEQ_1:def 4; then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1 - f2) by A2,SEQ_1:def 6; thus (r(#)(f1 - f2)).c = r * (f1 - f2).c by A2,SEQ_1:def 6 .= r * (f1.c - f2.c) by A4,SEQ_1:def 4 .= r * f1.c - r * f2.c by XCMPLX_1:40 .= (r(#)f1).c - r * f2.c by A3,SEQ_1:def 6 .= (r(#)f1).c - (r(#)f2).c by A3,SEQ_1:def 6 .= (r(#)f1 - r(#)f2).c by A1,A2,SEQ_1:def 4; end; hence thesis by A1,PARTFUN1:34; end; theorem f1-f2 = (-1)(#)(f2-f1) proof A1: dom (f1 - f2) = dom f2 /\ dom f1 by SEQ_1:def 4 .= dom (f2 - f1) by SEQ_1:def 4 .= dom ((-1)(#)(f2 - f1)) by SEQ_1:def 6; now let c such that A2: c in dom (f1-f2); A3: dom (f1 - f2) = dom f2 /\ dom f1 by SEQ_1:def 4 .= dom (f2 - f1) by SEQ_1:def 4; thus (f1 - f2).c = f1.c - f2.c by A2,SEQ_1:def 4 .= 1*(-(f2.c - f1.c)) by XCMPLX_1:143 .= (-1)*(f2.c - f1.c) by XCMPLX_1:176 .= (-1)*((f2 - f1).c) by A2,A3,SEQ_1:def 4 .= ((-1)(#)(f2 - f1)).c by A1,A2,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem f1 - (f2 + f3) = f1 - f2 - f3 proof A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by SEQ_1:def 4 .= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 3 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 - f2) /\ dom f3 by SEQ_1:def 4 .= dom (f1 - f2 - f3) by SEQ_1:def 4; now let c; assume A2: c in dom (f1 - (f2 + f3)); then c in dom (f1 - f2) /\ dom f3 by A1,SEQ_1:def 4; then A3: c in dom (f1 - f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 + f3) by A2,SEQ_1:def 4; then A4: c in dom (f2 + f3) by XBOOLE_0:def 3; thus (f1 - (f2 + f3)).c = f1.c - (f2 + f3).c by A2,SEQ_1:def 4 .= f1.c - (f2.c + f3.c) by A4,SEQ_1:def 3 .= f1.c - f2.c - f3.c by XCMPLX_1:36 .= (f1 - f2).c - f3.c by A3,SEQ_1:def 4 .= (f1 - f2 - f3).c by A1,A2,SEQ_1:def 4; end; hence thesis by A1,PARTFUN1:34; end; theorem Th33: 1(#)f = f proof A1: dom (1(#)f) = dom f by SEQ_1:def 6; now let c; assume c in dom (1(#)f); hence (1(#)f).c = 1 * f.c by SEQ_1:def 6 .= f.c; end; hence thesis by A1,PARTFUN1:34; end; theorem f1 - (f2 - f3) = f1 - f2 + f3 proof A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by SEQ_1:def 4 .= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 4 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 - f2) /\ dom f3 by SEQ_1:def 4 .= dom (f1 - f2 + f3) by SEQ_1:def 3; now let c; assume A2: c in dom (f1 - (f2 - f3)); then c in dom (f1 - f2) /\ dom f3 by A1,SEQ_1:def 3; then A3: c in dom (f1 - f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 - f3) by A2,SEQ_1:def 4; then A4: c in dom (f2 - f3) by XBOOLE_0:def 3; thus (f1 - (f2 - f3)).c = f1.c - (f2 - f3).c by A2,SEQ_1:def 4 .= f1.c - (f2.c - f3.c) by A4,SEQ_1:def 4 .= f1.c - f2.c + f3.c by XCMPLX_1:37 .= (f1 - f2).c + f3.c by A3,SEQ_1:def 4 .= (f1 - f2 + f3).c by A1,A2,SEQ_1:def 3; end; hence thesis by A1,PARTFUN1:34; end; theorem f1 + (f2 - f3) =f1 + f2 - f3 proof A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by SEQ_1:def 3 .= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 4 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 + f2) /\ dom f3 by SEQ_1:def 3 .= dom (f1 + f2 - f3) by SEQ_1:def 4; now let c; assume A2: c in dom (f1 + (f2 - f3)); then c in dom (f1 + f2) /\ dom f3 by A1,SEQ_1:def 4; then A3: c in dom (f1 + f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 - f3) by A2,SEQ_1:def 3; then A4: c in dom (f2 - f3) by XBOOLE_0:def 3; thus (f1 + (f2 - f3)).c = f1.c + (f2 - f3).c by A2,SEQ_1:def 3 .= f1.c + (f2.c - f3.c) by A4,SEQ_1:def 4 .= f1.c + f2.c - f3.c by XCMPLX_1:29 .= (f1 + f2).c - f3.c by A3,SEQ_1:def 3 .= (f1 + f2 - f3).c by A1,A2,SEQ_1:def 4; end; hence thesis by A1,PARTFUN1:34; end; theorem Th36: abs(f1(#)f2) = abs(f1)(#)abs(f2) proof A1: dom (abs(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 10 .= dom f1 /\ dom f2 by SEQ_1:def 5 .= dom f1 /\ dom (abs(f2)) by SEQ_1:def 10 .= dom (abs(f1)) /\ dom (abs(f2)) by SEQ_1:def 10 .= dom (abs(f1)(#)abs(f2)) by SEQ_1:def 5; now let c; assume A2: c in dom (abs(f1 (#) f2)); then c in dom (abs(f1)) /\ dom (abs(f2)) by A1,SEQ_1:def 5; then A3: c in dom (abs(f1)) & c in dom (abs(f2)) by XBOOLE_0:def 3; A4: c in dom (f1 (#) f2) by A2,SEQ_1:def 10; thus (abs(f1(#)f2)).c = abs((f1(#)f2).c) by A2,SEQ_1:def 10 .= abs(f1.c * f2.c) by A4,SEQ_1:def 5 .= abs(f1.c) * abs(f2.c) by ABSVALUE:10 .= ((abs(f1)).c) * abs(f2.c) by A3,SEQ_1:def 10 .= ((abs(f1)).c) * (abs(f2)).c by A3,SEQ_1:def 10 .= (abs(f1)(#)abs(f2)).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem abs(r(#)f) = abs(r)(#)abs(f) proof A1: dom (abs(r(#)f)) = dom (r(#)f) by SEQ_1:def 10 .= dom f by SEQ_1:def 6 .= dom (abs(f)) by SEQ_1:def 10 .= dom (abs(r)(#)abs(f)) by SEQ_1:def 6; now let c; assume A2: c in dom (abs(r(#)f)); then A3: c in dom (abs(f)) by A1,SEQ_1:def 6; A4: c in dom (r(#)f) by A2,SEQ_1:def 10; thus (abs(r(#)f)).c = abs((r(#)f).c) by A2,SEQ_1:def 10 .=abs(r*(f.c)) by A4,SEQ_1:def 6 .=abs(r)*abs(f.c) by ABSVALUE:10 .=abs(r)*(abs(f)).c by A3,SEQ_1:def 10 .=(abs(r)(#)abs(f)).c by A1,A2,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem Th38: -f = (-1)(#)f proof A1: dom (-f) = dom f by SEQ_1:def 7 .= dom ((-1)(#)f) by SEQ_1:def 6; now let c; assume A2: c in dom ((-1)(#)f); hence (-f).c = 1*(-f.c) by A1,SEQ_1:def 7 .= (-1) * f.c by XCMPLX_1:176 .= ((-1)(#)f).c by A2,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem Th39: -(-f) = f proof thus -(-f) = (-1)(#)(-f) by Th38 .= (-1)(#)((-1)(#)f) by Th38 .= ((-1)*(-1))(#)f by Th29 .= f by Th33; end; theorem Th40: f1 - f2 = f1 + -f2 proof A1: dom (f1 - f2) = dom f1 /\ dom f2 by SEQ_1:def 4 .= dom f1 /\ dom (-f2) by SEQ_1:def 7 .= dom (f1 + -f2) by SEQ_1:def 3; now let c; assume A2: c in dom (f1+-f2); then c in dom f1 /\ dom (-f2) by SEQ_1:def 3; then A3: c in dom (-f2) by XBOOLE_0:def 3; thus (f1 + -f2).c = f1.c + (-f2).c by A2,SEQ_1:def 3 .= f1.c + -(f2.c) by A3,SEQ_1:def 7 .= f1.c - f2.c by XCMPLX_0:def 8 .= (f1-f2).c by A1,A2,SEQ_1:def 4; end; hence thesis by A1,PARTFUN1:34; end; theorem f1 - (-f2) = f1 + f2 proof thus f1 - (-f2) = f1 + (-(-f2)) by Th40 .= f1 + f2 by Th39; end; theorem Th42: f^^ = f|(dom (f^)) proof A1: dom (f^^) = dom (f|(dom (f^))) by Th16; now let c; assume A2: c in dom (f^^); then c in dom f /\ dom (f^) by A1,RELAT_1:90; then A3:c in dom f & c in dom (f^) by XBOOLE_0:def 3; thus (f^^).c = ((f^).c)" by A2,Def8 .= ((f.c)")" by A3,Def8 .= (f|(dom (f^))).c by A1,A2,FUNCT_1:70; end; hence thesis by A1,PARTFUN1:34; end; theorem Th43: (f1(#)f2)^ = (f1^)(#)(f2^) proof A1: dom ((f1(#)f2)^) = dom (f1(#)f2) \ (f1(#)f2)"{0} by Def8 .= (dom f1 \ f1"{0}) /\ (dom f2 \ (f2)"{0}) by Th12 .= dom (f1^) /\ (dom f2 \ (f2)"{0}) by Def8 .= dom (f1^) /\ dom (f2^) by Def8 .= dom ((f1^) (#) (f2^)) by SEQ_1:def 5; now let c; assume A2: c in dom ((f1(#)f2)^); then c in dom (f1^) /\ dom (f2^) by A1,SEQ_1:def 5; then A3: c in dom (f1^) & c in dom (f2^) by XBOOLE_0:def 3; c in dom (f1(#)f2) \ (f1(#)f2)"{0} by A2,Def8; then A4: c in dom (f1(#)f2) by XBOOLE_0:def 4; thus ((f1(#)f2)^).c = ((f1(#)f2).c)" by A2,Def8 .= (f1.c * f2.c)" by A4,SEQ_1:def 5 .= (f1.c)"* (f2.c)" by XCMPLX_1:205 .= ((f1^).c)*(f2.c)" by A3,Def8 .= ((f1^).c) *((f2^).c) by A3,Def8 .= ((f1^) (#) (f2^)).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem Th44: r<>0 implies (r(#)f)^ = r" (#) (f^) proof assume A1: r<>0; A2: dom ((r(#)f)^) = dom (r(#)f) \ (r(#)f)"{0} by Def8 .= dom (r(#)f) \ f"{0} by A1,Th17 .= dom f \ f"{0} by SEQ_1:def 6 .= dom (f^) by Def8 .= dom (r"(#)(f^)) by SEQ_1:def 6; now let c; assume A3: c in dom ((r(#)f)^); then c in dom (r(#)f) \ (r(#)f)"{0} by Def8; then A4: c in dom (r(#)f) by XBOOLE_0:def 4; A5: c in dom (f^) by A2,A3,SEQ_1:def 6; thus ((r(#)f)^).c = ((r(#)f).c)" by A3,Def8 .= (r*(f.c))" by A4,SEQ_1:def 6 .= r"* (f.c)" by XCMPLX_1:205 .= r"* ((f^).c) by A5,Def8 .= (r" (#) (f^)).c by A2,A3,SEQ_1:def 6; end; hence thesis by A2,PARTFUN1:34; end; theorem Th45: (-f)^ = (-1)(#)(f^) proof thus (-f)^=((-1)(#)f)^ by Th38 .= (-1)(#)(f^) by Lm1,Th44; end; theorem Th46: (abs(f))^ = abs((f^)) proof A1: dom ((abs(f))^) = dom (abs(f)) \ (abs(f))"{0} by Def8 .= dom f \ (abs(f))"{0} by SEQ_1:def 10 .= dom f \ f"{0} by Th15 .= dom (f^) by Def8 .= dom (abs((f^))) by SEQ_1:def 10; now let c; assume A2: c in dom ((abs(f))^); then c in dom (abs(f)) \ (abs(f))"{0} by Def8; then A3: c in dom (abs(f)) by XBOOLE_0:def 4; A4: c in dom (f^) by A1,A2,SEQ_1:def 10; thus ((abs(f))^).c = ((abs(f)).c)" by A2,Def8 .= (abs(f.c ))" by A3,SEQ_1:def 10 .= 1/abs(f.c ) by XCMPLX_1:217 .= abs(1/f.c ) by ABSVALUE:15 .= abs((f.c)" ) by XCMPLX_1:217 .= abs((f^).c ) by A4,Def8 .= (abs((f^))).c by A1,A2,SEQ_1:def 10; end; hence thesis by A1,PARTFUN1:34; end; theorem Th47: f/g = f(#) (g^) proof A1: dom (f/g) = dom f /\ (dom g \ g"{0}) by Def4 .= dom f /\ dom (g^) by Def8 .= dom (f(#)(g^)) by SEQ_1:def 5; now let c; assume A2: c in dom (f/g); then c in dom f /\ (dom g \ g"{0}) by Def4; then A3: c in dom f /\ dom (g^) by Def8; then A4: c in dom (g^) by XBOOLE_0:def 3; A5: c in dom (f (#) (g^)) by A3,SEQ_1:def 5; thus (f/g).c = f.c * (g.c)" by A2,Def4 .= f.c * (g^).c by A4,Def8 .= (f (#) (g^)).c by A5,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem Th48: r(#)(g/f) = (r(#)g)/f proof thus r(#)(g/f) = r(#)(g(#)(f^)) by Th47 .= (r(#)g)(#)(f^) by Th24 .= (r(#)g)/f by Th47; end; theorem (f/g)(#)g = (f|dom(g^)) proof A1: dom (g^) c= dom g by Th11; A2: dom ((f/g)(#)g) = dom (f/g) /\ dom g by SEQ_1:def 5 .= dom f /\ (dom g \ g"{0}) /\ dom g by Def4 .= dom f /\ ((dom g \ g"{0}) /\ dom g) by XBOOLE_1:16 .= dom f /\ (dom (g^) /\ dom g) by Def8 .= dom f /\ dom (g^) by A1,XBOOLE_1:28 .= dom (f|(dom (g^))) by RELAT_1:90; now let c; assume A3: c in dom ((f/g)(#)g); then A4: c in dom f /\ dom (g^) by A2,RELAT_1:90; then A5: c in dom (f(#)(g^)) by SEQ_1:def 5; A6: c in dom f & c in dom (g^) by A4,XBOOLE_0:def 3; then A7: g.c <> 0 by Th13; thus ((f/g)(#)g).c = ((f/g).c) * g.c by A3,SEQ_1:def 5 .= (f(#)(g^)).c * g.c by Th47 .= (f.c) *((g^).c) * g.c by A5,SEQ_1:def 5 .= (f.c)*(g.c)"*g.c by A6,Def8 .= (f.c)*((g.c)" * (g.c)) by XCMPLX_1:4 .= (f.c)*1 by A7,XCMPLX_0:def 7 .= (f|(dom (g^))).c by A2,A3,FUNCT_1:70; end; hence thesis by A2,PARTFUN1:34; end; theorem Th50: (f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1) proof A1: dom ((f/g)(#)(f1/g1)) = dom (f/g) /\ dom (f1/g1) by SEQ_1:def 5 .= dom f /\ (dom g \ g"{0}) /\ dom (f1/g1) by Def4 .= dom f /\ (dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0})) by Def4 .= dom f /\ ((dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0}))) by XBOOLE_1:16 .= dom f /\ (dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0}))) by XBOOLE_1:16 .= dom f /\ dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by XBOOLE_1:16 .= dom (f(#)f1) /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by SEQ_1:def 5 .= dom (f(#)f1) /\ (dom (g(#)g1) \ (g(#)g1)"{0}) by Th12 .= dom ((f(#)f1)/(g(#)g1)) by Def4; now let c; assume A2: c in dom ((f/g)(#)(f1/g1)); then c in dom (f/g) /\ dom (f1/g1) by SEQ_1:def 5; then c in dom (f (#)(g^)) /\ dom (f1/g1) by Th47; then c in dom (f (#)(g^)) /\ dom (f1(#)(g1^)) by Th47; then A3: c in dom (f (#)(g^)) & c in dom (f1(#)(g1^)) by XBOOLE_0:def 3; then c in dom f /\ dom(g^) & c in dom f1 /\ dom(g1^) by SEQ_1:def 5; then c in dom f & c in dom(g^) & c in dom f1 & c in dom(g1^) by XBOOLE_0:def 3 ; then c in dom f /\ dom f1 & c in dom (g^) /\ dom (g1^) by XBOOLE_0:def 3; then A4: c in dom (f(#)f1) & c in dom((g^)(#)(g1^)) by SEQ_1:def 5; then c in dom (f(#)f1) & c in dom((g(#)g1)^) by Th43; then c in dom (f(#)f1) /\ dom((g(#)g1)^) by XBOOLE_0:def 3; then A5: c in dom ((f(#)f1)(#)((g(#)g1)^)) by SEQ_1:def 5; thus ((f/g)(#)(f1/g1)).c = ((f/g).c)* (f1/g1).c by A2,SEQ_1:def 5 .= ((f(#)(g^)).c) * (f1/g1).c by Th47 .= ((f(#)(g^)).c) * (f1(#)(g1^)).c by Th47 .= (f.c) * ((g^).c) * (f1(#)(g1^)).c by A3,SEQ_1:def 5 .= (f.c) * ((g^).c) * ((f1.c)* (g1^).c) by A3,SEQ_1:def 5 .= (f.c) * ((g^).c) * (f1.c) * (g1^).c by XCMPLX_1:4 .= (f.c) * ((f1.c) * (g^).c) * (g1^).c by XCMPLX_1:4 .= (f.c) * (((f1.c) * (g^).c) * (g1^).c) by XCMPLX_1:4 .= (f.c) * ((f1.c) * (((g^).c) * (g1^).c)) by XCMPLX_1:4 .= (f.c) * ((f1.c) * ((g^)(#)(g1^)).c) by A4,SEQ_1:def 5 .= (f.c) * (f1.c) * ((g^)(#)(g1^)).c by XCMPLX_1:4 .= (f.c) * (f1.c) * ((g(#)g1)^).c by Th43 .= ((f(#)f1).c) * ((g(#)g1)^).c by A4,SEQ_1:def 5 .= ((f(#)f1)(#)((g(#)g1)^)).c by A5,SEQ_1:def 5 .= ((f(#)f1)/(g(#)g1)).c by Th47; end; hence thesis by A1,PARTFUN1:34; end; theorem Th51: (f1/f2)^ = (f2|dom(f2^))/f1 proof thus (f1/f2)^ = (f1(#)(f2^))^ by Th47 .= (f1^)(#)(f2^^) by Th43 .= (f2|dom(f2^))(#)(f1^) by Th42 .= (f2|dom(f2^))/f1 by Th47; end; theorem Th52: g (#) (f1/f2) = (g (#) f1)/f2 proof thus g (#) (f1/f2) = g (#) (f1 (#) (f2^)) by Th47 .= g (#) f1 (#) (f2^) by Th21 .= (g (#) f1)/f2 by Th47; end; theorem g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1 proof thus g/(f1/f2) = g (#) ((f1/f2)^) by Th47 .= g (#) ((f2|dom(f2^))/f1) by Th51 .= (g (#) (f2|dom(f2^)))/f1 by Th52; end; theorem -f/g = (-f)/g & f/(-g) = -f/g proof thus -f/g = (-1)(#)(f/g) by Th38 .= ((-1) (#) f)/g by Th48 .= (-f)/g by Th38; thus f/(-g) = f (#) ((-g)^) by Th47 .= f (#) ((-1) (#) (g^)) by Th45 .= (-1) (#) (f (#) (g^)) by Th25 .= -(f (#) (g^)) by Th38 .= -(f/g) by Th47; end; theorem f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f proof thus f1/f + f2/f = f1(#)(f^) +f2/f by Th47 .= f1(#)(f^) + f2(#)(f^) by Th47 .= (f1+f2) (#) (f^) by Th22 .= (f1+f2)/f by Th47; thus f1/f - f2/f = f1(#)(f^) - f2/f by Th47 .= f1(#)(f^) -f2(#)(f^) by Th47 .= (f1-f2)(#)(f^) by Th26 .= (f1-f2)/f by Th47; end; theorem Th56: f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g) proof A1: dom ((f1/f) + (g1/g)) = dom (f1/f) /\ dom (g1/g) by SEQ_1:def 3 .= dom f1 /\ (dom f \ f"{0}) /\ dom (g1/g) by Def4 .= dom f1 /\ (dom f \ f"{0}) /\ (dom g1 /\ (dom g \ g"{0})) by Def4 .= dom f1 /\ (dom f /\ (dom f \ f"{0})) /\ (dom g1 /\ (dom g \ g"{0})) by Th11 .= dom f /\ (dom f \ f"{0}) /\ dom f1 /\ (dom g /\ (dom g \ g"{0}) /\ dom g1) by Th11 .= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0}) /\ dom g1)) by XBOOLE_1:16 .= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0})) /\ dom g1) by XBOOLE_1:16 .= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ dom g /\ (dom g \ g"{0}) /\ dom g1) by XBOOLE_1:16 .= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\ (dom g \ g"{0}) /\ dom g1) by SEQ_1:def 5 .= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\ (dom g1 /\ (dom g \ g"{0}))) by XBOOLE_1:16 .= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ dom f /\ (dom g1 /\ (dom g \ g"{0}))) by XBOOLE_1:16 .= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom f /\ (dom g1 /\ (dom g \ g"{0})))) by XBOOLE_1:16 .= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom g1 /\ dom f /\ (dom g \ g"{0}))) by XBOOLE_1:16 .= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom (g1(#)f) /\ (dom g \ g"{0}))) by SEQ_1:def 5 .= dom (f1(#)g) /\ (dom (g1(#)f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0}))) by XBOOLE_1:16 .= dom (f1(#)g) /\ dom (g1(#) f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0})) by XBOOLE_1:16 .= dom (f1(#)g + g1(#)f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0})) by SEQ_1:def 3 .= dom (f1(#)g + g1(#)f) /\ (dom (f(#)g) \ (f(#)g)"{0}) by Th12 .= dom ((f1(#)g + g1(#)f)/(f(#)g)) by Def4; now let c; assume A2: c in dom ((f1/f) + (g1/g)); then A3: c in dom (f1/f) /\ dom (g1/g) by SEQ_1:def 3; then A4: c in dom (f1/f) & c in dom (g1/g) by XBOOLE_0:def 3; c in dom (f1 (#)(f^)) /\ dom (g1/g) by A3,Th47; then c in dom (f1 (#)(f^)) /\ dom (g1(#)(g^)) by Th47; then c in dom (f1 (#)(f^)) & c in dom (g1(#)(g^)) by XBOOLE_0:def 3; then c in dom f1 /\ dom(f^) & c in dom g1 /\ dom(g^) by SEQ_1:def 5; then A5: c in dom f1 & c in dom(f^) & c in dom g1 & c in dom(g^) by XBOOLE_0:def 3; then A6: f.c <> 0 & g.c <> 0 by Th13; c in dom f1 /\ dom g1 & c in dom (f^) /\ dom (g^) by A5,XBOOLE_0:def 3; then c in dom f1 /\ dom g1 & c in dom ((f^)(#)(g^)) by SEQ_1:def 5; then A7: c in dom f1 /\ dom g1 & c in dom ((f(#)g)^) by Th43; A8: dom (g^) c= dom g & dom (f^) c= dom f by Th11; then c in dom f /\ dom g by A5,XBOOLE_0:def 3; then A9:c in dom (f(#)g) by SEQ_1:def 5; c in dom f1 /\ dom g & c in dom g1 /\ dom f by A5,A8,XBOOLE_0:def 3; then A10: c in dom (f1(#)g) & c in dom (g1(#)f) by SEQ_1:def 5; then c in dom (f1(#)g) /\ dom (g1(#)f) by XBOOLE_0:def 3; then A11: c in dom (f1(#)g + g1(#)f) by SEQ_1:def 3; then c in dom (f1(#)g + g1(#)f) /\ dom ((f(#)g)^) by A7,XBOOLE_0:def 3; then c in dom ((f1(#)g + g1(#)f)(#)((f(#)g)^)) by SEQ_1:def 5; then A12: c in dom ((f1(#)g + g1(#)f)/(f(#)g)) by Th47; thus (f1/f + g1/g).c = (f1/f).c + (g1/g).c by A2,SEQ_1:def 3 .= (f1.c) * (f.c)" + (g1/g).c by A4,Def4 .= (f1.c) *(1*(f.c)") + (g1.c) * 1 * (g.c)" by A4,Def4 .= (f1.c) *((g.c) *(g.c)"* (f.c)") + (g1.c) * (1 * (g.c)") by A6,XCMPLX_0:def 7 .= (f1.c) *((g.c) *(g.c)"* (f.c)") + (g1.c) * ((f.c) *(f.c)" * (g.c)") by A6,XCMPLX_0:def 7 .= (f1.c) *(g.c *((g.c)"* (f.c)")) + (g1.c) * ((f.c) *(f.c)" * (g.c)") by XCMPLX_1:4 .= (f1.c) *((g.c) *((g.c)"* (f.c)")) + (g1.c) * ((f.c) *((f.c)" * (g.c)")) by XCMPLX_1:4 .= (f1.c) *((g.c) *((g.c * f.c)")) + (g1.c) * ((f.c) *((f.c)" * (g.c)")) by XCMPLX_1:205 .= (f1.c) *((g.c) *((f.c* g.c)")) + (g1.c) * ((f.c) *((f.c * g.c)")) by XCMPLX_1:205 .= (f1.c) *((g.c) * ((f(#)g).c)") + (g1.c) * ((f.c) *((f.c * g.c)")) by A9,SEQ_1:def 5 .= (f1.c) *((g.c) *((f(#)g).c)") + (g1.c) *((f.c) *((f(#)g).c)") by A9,SEQ_1:def 5 .= (f1.c) *(g.c) * ((f(#)g).c)" + (g1.c) * ((f.c) * ((f(#) g).c)") by XCMPLX_1:4 .= (f1.c) *(g.c) * ((f(#)g).c)" + (g1.c) * (f.c) * ((f(#)g).c)" by XCMPLX_1:4 .= (f1(#)g).c * ((f(#)g).c)" + (g1.c) *f.c *((f(#)g).c)" by A10,SEQ_1:def 5 .= (f1(#)g).c * ((f(#)g).c)" + (g1(#)f).c *((f(#)g).c)" by A10,SEQ_1:def 5 .= ((f1(#)g).c + (g1(#)f).c) *((f(#)g).c)" by XCMPLX_1:8 .= (f1(#)g + g1(#)f).c *((f(#)g).c)" by A11,SEQ_1:def 3 .= ((f1(#)g + g1(#)f)/(f(#)g)).c by A12,Def4; end; hence f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g) by A1,PARTFUN1:34; end; theorem (f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1) proof thus (f/g)/(f1/g1) = (f/g)(#)((f1/g1)^) by Th47 .= (f/g)(#)(((g1|dom(g1^)))/f1) by Th51 .= (f(#)(g1|dom(g1^)))/(g(#)f1) by Th50; end; theorem f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g) proof thus f1/f - g1/g = f1/f +- g1/g by Th40 .= f1/f + (-1)(#) (g1/g) by Th38 .= f1/f + ((-1)(#) g1)/g by Th48 .= (f1(#)g + (-1)(#) g1(#)f)/(f(#)g) by Th56 .= (f1(#)g + (-1)(#) (g1(#)f))/(f(#)g) by Th24 .= (f1(#)g + - (g1(#)f))/(f(#)g) by Th38 .= (f1(#)g - (g1(#)f))/(f(#)g) by Th40; end; theorem abs(f1/f2) = abs(f1)/abs(f2) proof thus abs(f1/f2) = abs(f1(#)(f2^)) by Th47 .= abs(f1)(#)abs((f2^)) by Th36 .= abs(f1)(#)((abs(f2))^) by Th46 .= abs(f1)/abs(f2) by Th47; end; theorem Th60: (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X proof A1: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ (X /\ X) by SEQ_1:def 3 .= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16 .= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16 .= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:90 .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16 .= dom (f1|X) /\ dom (f2|X) by RELAT_1:90 .= dom ((f1|X)+(f2|X)) by SEQ_1:def 3; now let c; assume A2: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A3: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90; then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3; then A5: c in dom ((f1|X) + (f2|X)) by SEQ_1:def 3; thus ((f1+f2)|X).c = (f1+f2).c by A2,FUNCT_1:70 .= (f1.c) + (f2.c) by A3,SEQ_1:def 3 .= ((f1|X).c) + (f2.c) by A4,FUNCT_1:70 .= ((f1|X).c) + ((f2|X).c) by A4,FUNCT_1:70 .= ((f1|X)+(f2|X)).c by A5,SEQ_1:def 3; end; hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN1:34; A6: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by SEQ_1:def 3 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:90 .= dom ((f1|X)+ f2) by SEQ_1:def 3; now let c; assume A7: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A8: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3; then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90; then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3; then A10: c in dom ((f1|X) + f2) by SEQ_1:def 3; thus ((f1+f2)|X).c = (f1+f2).c by A7,FUNCT_1:70 .= (f1.c) +(f2.c) by A8,SEQ_1:def 3 .= ((f1|X).c) +(f2.c) by A9,FUNCT_1:70 .= ((f1|X)+f2).c by A10,SEQ_1:def 3; end; hence (f1+f2)|X = f1|X + f2 by A6,PARTFUN1:34; A11: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by SEQ_1:def 3 .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16 .= dom f1 /\ dom (f2|X) by RELAT_1:90 .= dom (f1 + (f2|X)) by SEQ_1:def 3; now let c; assume A12: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A13: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3; then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90; then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3; then A15: c in dom (f1 + (f2|X)) by SEQ_1:def 3; thus ((f1+f2)|X).c = (f1+f2).c by A12,FUNCT_1:70 .= (f1.c) +(f2.c) by A13,SEQ_1:def 3 .= (f1.c) +((f2|X).c) by A14,FUNCT_1:70 .= (f1+(f2|X)).c by A15,SEQ_1:def 3; end; hence thesis by A11,PARTFUN1:34; end; theorem Th61: (f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#) f2|X proof A1: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ (X /\ X) by SEQ_1:def 5 .= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16 .= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16 .= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:90 .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16 .= dom (f1|X) /\ dom (f2|X) by RELAT_1:90 .= dom ((f1|X)(#)(f2|X)) by SEQ_1:def 5; now let c; assume A2: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A3: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 5; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90; then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3; then A5: c in dom ((f1|X) (#) (f2|X)) by SEQ_1:def 5; thus ((f1(#)f2)|X).c = (f1(#)f2).c by A2,FUNCT_1:70 .= (f1.c) *(f2.c) by A3,SEQ_1:def 5 .= ((f1|X).c) *(f2.c) by A4,FUNCT_1:70 .= ((f1|X).c) *((f2|X).c) by A4,FUNCT_1:70 .= ((f1|X)(#)(f2|X)).c by A5,SEQ_1:def 5; end; hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN1:34; A6: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by SEQ_1:def 5 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:90 .= dom ((f1|X)(#) f2) by SEQ_1:def 5; now let c; assume A7: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A8: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 5; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3; then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90; then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3; then A10: c in dom ((f1|X) (#) f2) by SEQ_1:def 5; thus ((f1(#)f2)|X).c = (f1(#)f2).c by A7,FUNCT_1:70 .= (f1.c) *(f2.c) by A8,SEQ_1:def 5 .= ((f1|X).c) *(f2.c) by A9,FUNCT_1:70 .= ((f1|X)(#)f2).c by A10,SEQ_1:def 5; end; hence (f1(#)f2)|X = f1|X (#) f2 by A6,PARTFUN1:34; A11: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by SEQ_1:def 5 .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16 .= dom f1 /\ dom (f2|X) by RELAT_1:90 .= dom (f1 (#) (f2|X)) by SEQ_1:def 5; now let c; assume A12: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A13: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by SEQ_1:def 5; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3; then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90; then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3; then A15: c in dom (f1 (#) (f2|X)) by SEQ_1:def 5; thus ((f1(#)f2)|X).c = (f1(#)f2).c by A12,FUNCT_1:70 .= (f1.c) *(f2.c) by A13,SEQ_1:def 5 .= (f1.c) *((f2|X).c) by A14,FUNCT_1:70 .= (f1(#)(f2|X)).c by A15,SEQ_1:def 5; end; hence thesis by A11,PARTFUN1:34; end; theorem Th62: (-f)|X = -(f|X) & (f^)|X = (f|X)^ & (abs(f))|X = abs((f|X)) proof A1: dom ((-f)|X) = dom (-f) /\ X by RELAT_1:90 .= dom f /\ X by SEQ_1:def 7 .= dom (f|X) by RELAT_1:90 .= dom (-(f|X)) by SEQ_1:def 7; now let c; assume A2: c in dom ((-f)|X); then c in dom (-f) /\ X by RELAT_1:90; then A3: c in dom (-f) & c in X by XBOOLE_0:def 3; then c in dom f by SEQ_1:def 7; then c in dom f /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f|X) by RELAT_1:90; then A5: c in dom (-(f|X)) by SEQ_1:def 7; thus ((-f)|X).c = (-f).c by A2,FUNCT_1:70 .= -(f.c) by A3,SEQ_1:def 7 .= -((f|X).c) by A4,FUNCT_1:70 .= (-(f|X)).c by A5,SEQ_1:def 7; end; hence (-f)|X = -(f|X) by A1,PARTFUN1:34; A6: dom ((f|X)^) c= dom (f|X) by Th11; A7: dom ((f^)|X) = dom (f^) /\ X by RELAT_1:90 .= (dom f \ f"{0}) /\ X by Def8 .= dom f /\ X \ f"{0} /\ X by XBOOLE_1:50 .= dom (f|X) \ X /\ f"{0} by RELAT_1:90 .= dom (f|X) \ (f|X)"{0} by FUNCT_1:139 .= dom ((f|X)^) by Def8; now let c; assume A8: c in dom ((f^)|X); then c in dom (f^) /\ X by RELAT_1:90; then A9: c in dom (f^) & c in X by XBOOLE_0:def 3; thus ((f^)|X).c = (f^).c by A8,FUNCT_1:70 .= (f.c)" by A9,Def8 .= ((f|X).c)" by A6,A7,A8,FUNCT_1:70 .= ((f|X)^).c by A7,A8,Def8; end; hence (f^)|X = (f|X)^ by A7,PARTFUN1:34; A10: dom ((abs(f))|X) = dom (abs(f)) /\ X by RELAT_1:90 .= dom f /\ X by SEQ_1:def 10 .= dom (f|X) by RELAT_1:90 .= dom (abs((f|X))) by SEQ_1:def 10; now let c; assume A11: c in dom ((abs(f))|X); then c in dom (abs(f)) /\ X by RELAT_1:90; then A12: c in dom (abs(f)) & c in X by XBOOLE_0:def 3; A13: c in dom (f|X) by A10,A11,SEQ_1:def 10; thus ((abs(f))|X).c = (abs(f)).c by A11,FUNCT_1:70 .= abs(f.c) by A12,SEQ_1:def 10 .= abs((f|X).c) by A13,FUNCT_1:70 .= (abs((f|X))).c by A10,A11,SEQ_1:def 10; end; hence thesis by A10,PARTFUN1:34; end; theorem (f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X proof thus (f1-f2)|X = (f1+-f2)|X by Th40 .= (f1|X)+ (-f2)|X by Th60 .= (f1|X)+ -(f2|X) by Th62 .= (f1|X) - (f2|X) by Th40; thus (f1-f2)|X = (f1+-f2)|X by Th40 .= (f1|X)+ -f2 by Th60 .= (f1|X) - f2 by Th40; thus (f1-f2)|X = (f1+-f2)|X by Th40 .= f1+ (-f2)|X by Th60 .= f1 +- (f2|X) by Th62 .= f1 - (f2|X) by Th40; end; theorem (f1/f2)|X = f1|X / f2|X & (f1/f2)|X = f1|X / f2 &(f1/f2)|X = f1 / f2|X proof thus (f1/f2)|X = (f1(#)(f2^))|X by Th47 .= (f1|X) (#) (f2^|X) by Th61 .= (f1|X) (#) ((f2|X)^) by Th62 .= (f1|X)/(f2|X) by Th47; thus (f1/f2)|X = (f1(#)(f2^))|X by Th47 .= (f1|X) (#) (f2^) by Th61 .= (f1|X)/f2 by Th47; thus (f1/f2)|X = (f1(#)(f2^))|X by Th47 .= f1 (#) (f2^)|X by Th61 .= f1 (#) ((f2|X)^) by Th62 .= f1/(f2|X) by Th47; end; theorem (r(#)f)|X = r(#)(f|X) proof A1: dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:90 .= dom f /\ X by SEQ_1:def 6 .= dom (f|X) by RELAT_1:90 .= dom (r(#)(f|X)) by SEQ_1:def 6; now let c; assume A2: c in dom ((r(#)f)|X); then c in dom (r(#)f) /\ X by RELAT_1:90; then A3: c in dom (r(#)f) & c in X by XBOOLE_0:def 3; then c in dom f by SEQ_1:def 6; then c in dom f /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f|X) by RELAT_1:90; then A5: c in dom (r(#)(f|X)) by SEQ_1:def 6; thus ((r(#)f)|X).c = (r(#)f).c by A2,FUNCT_1:70 .= r*(f.c) by A3,SEQ_1:def 6 .= r*(f|X).c by A4,FUNCT_1:70 .= (r(#)(f|X)).c by A5,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; :: :: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL :: theorem Th66: (f1 is total & f2 is total iff f1+f2 is total) & (f1 is total & f2 is total iff f1-f2 is total) & (f1 is total & f2 is total iff f1(#)f2 is total) proof thus f1 is total & f2 is total iff f1+f2 is total proof thus f1 is total & f2 is total implies f1+f2 is total proof assume f1 is total & f2 is total; then dom f1 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1+f2) = C /\ C by SEQ_1:def 3 .= C; end; assume f1+f2 is total; then dom (f1+f2) = C by PARTFUN1:def 4; then dom f1 /\ dom f2 = C by SEQ_1:def 3; then C c= dom f1 & C c= dom f2 by XBOOLE_1:17; hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10; end; thus f1 is total & f2 is total iff f1-f2 is total proof thus f1 is total & f2 is total implies f1-f2 is total proof assume f1 is total & f2 is total; then dom f1 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1-f2) = C /\ C by SEQ_1:def 4 .= C; end; assume f1-f2 is total; then dom (f1-f2) = C by PARTFUN1:def 4; then dom f1 /\ dom f2 = C by SEQ_1:def 4; then C c= dom f1 & C c= dom f2 by XBOOLE_1:17; hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10; end; thus f1 is total & f2 is total implies f1(#)f2 is total proof assume f1 is total & f2 is total; then dom f1 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1(#)f2) = C /\ C by SEQ_1:def 5 .= C; end; assume f1(#)f2 is total; then dom (f1(#)f2) = C by PARTFUN1:def 4; then dom f1 /\ dom f2 = C by SEQ_1:def 5; then C c= dom f1 & C c= dom f2 by XBOOLE_1:17; hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10; end; theorem Th67: f is total iff r(#)f is total proof thus f is total implies r(#)f is total proof assume f is total; then dom f = C by PARTFUN1:def 4; hence dom (r(#)f) = C by SEQ_1:def 6; end; assume r(#)f is total; then dom (r(#)f) = C by PARTFUN1:def 4; hence dom f = C by SEQ_1:def 6; end; theorem Th68: f is total iff -f is total proof thus f is total implies -f is total proof assume A1: f is total; -f = (-1)(#) f by Th38; hence -f is total by A1,Th67 ; end; assume A2: -f is total; -f = (-1)(#)f by Th38; hence f is total by A2,Th67; end; theorem Th69: f is total iff abs(f) is total proof thus f is total implies abs(f) is total proof assume f is total; then dom f = C by PARTFUN1:def 4; hence dom (abs(f)) = C by SEQ_1:def 10; end; assume abs(f) is total; then dom (abs(f)) = C by PARTFUN1:def 4; hence dom f = C by SEQ_1:def 10; end; theorem Th70: f^ is total iff f"{0} = {} & f is total proof thus f^ is total implies f"{0} = {} & f is total proof assume f^ is total; then A1: dom (f^) = C by PARTFUN1:def 4; f"{0} c= C; then f"{0} c= dom f \ f"{0} by A1,Def8; hence f"{0} = {} by XBOOLE_1:38; then C = dom f \ {} by A1,Def8; hence dom f = C; end; assume A2: f"{0} = {} & f is total; thus dom (f^) = dom f \ f"{0} by Def8 .= C by A2,PARTFUN1:def 4; end; theorem Th71: f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total proof thus f1 is total & f2"{0} = {} & f2 is total implies f1/f2 is total proof assume A1: f1 is total & f2"{0} = {} & f2 is total; then f2^ is total by Th70; then f1(#)(f2^) is total by A1,Th66; hence f1/f2 is total by Th47; end; assume f1/f2 is total; then A2: f1(#)(f2^) is total by Th47; hence f1 is total by Th66; f2^ is total by A2,Th66; hence thesis by Th70; end; theorem f1 is total & f2 is total implies (f1+f2).c = f1.c + f2.c & (f1-f2).c = f1.c - f2.c & (f1(#)f2).c = f1.c * f2.c proof assume A1: f1 is total & f2 is total; then f1+f2 is total by Th66; then dom (f1+f2) = C by PARTFUN1:def 4; hence (f1+f2).c = f1.c + f2.c by SEQ_1:def 3; f1-f2 is total by A1,Th66; then dom (f1-f2) = C by PARTFUN1:def 4; hence (f1-f2).c = f1.c - f2.c by SEQ_1:def 4; f1(#)f2 is total by A1,Th66; then dom (f1(#)f2) = C by PARTFUN1:def 4; hence (f1(#)f2).c = f1.c * f2.c by SEQ_1:def 5; end; theorem f is total implies (r(#)f).c = r * (f.c) proof assume f is total; then r(#)f is total by Th67; then dom (r(#)f) = C by PARTFUN1:def 4; hence (r(#)f).c = r * (f.c) by SEQ_1:def 6; end; theorem f is total implies (-f).c = - f.c & (abs(f)).c = abs( f.c ) proof assume A1: f is total; then -f is total by Th68; then dom (-f) = C by PARTFUN1:def 4; hence (-f).c = - f.c by SEQ_1:def 7; abs(f) is total by A1,Th69; then dom (abs(f)) = C by PARTFUN1:def 4; hence (abs(f)).c = abs( f.c ) by SEQ_1:def 10; end; theorem f^ is total implies (f^).c = (f.c)" proof assume f^ is total; then dom (f^) = C by PARTFUN1:def 4; hence (f^).c = (f.c)" by Def8; end; theorem f1 is total & f2^ is total implies (f1/f2).c = f1.c *(f2.c)" proof assume f1 is total & f2^ is total; then f1 is total & f2"{0} = {} & f2 is total by Th70; then f1/f2 is total by Th71; then dom (f1/f2) = C by PARTFUN1:def 4; hence thesis by Def4; end; :: :: CHARCTERISTIC FUNCTION OF A SUBSET OF A DOMAIN :: definition let X,C be set; redefine func chi(X,C) -> PartFunc of C,REAL; coherence proof A1: dom chi(X,C) =C by FUNCT_3:def 3; now let x; assume x in rng chi(X,C); then x = 0 or x = 1 by TARSKI:def 2; hence x in REAL; end; then rng chi(X,C) c= REAL by TARSKI:def 3; hence thesis by A1,RELSET_1:11; end; end; theorem Th77: f= chi(X,C) iff ( dom f = C & for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0)) proof thus f= chi(X,C) implies (dom f = C & for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0)) by FUNCT_3:def 3; assume A1: dom f = C & for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0); then for x st x in C holds (x in X implies (f qua Function).x = 1) & (not x in X implies (f qua Function).x = 0); hence thesis by A1,FUNCT_3:def 3; end; theorem chi(X,C) is total proof dom chi(X,C) = C by Th77; hence thesis by PARTFUN1:def 4; end; theorem c in X iff chi(X,C).c = 1 by Th77; theorem not c in X iff chi(X,C).c = 0 by Th77; theorem c in C \ X iff chi(X,C).c = 0 proof thus c in C \ X implies chi(X,C).c = 0 proof assume c in C \ X; then not c in X by XBOOLE_0:def 4; hence thesis by Th77; end; assume chi(X,C).c = 0; then not c in X by Th77; hence thesis by XBOOLE_0:def 4; end; canceled; theorem chi(C,C).c = 1 by Th77; theorem Th84: chi(X,C).c <> 1 iff chi(X,C).c = 0 proof thus chi(X,C).c <> 1 implies chi(X,C).c = 0 proof assume A1: chi(X,C).c <> 1; c in C; then c in dom chi(X,C) by Th77; then A2: chi(X,C).c in rng chi(X,C) by FUNCT_1:def 5; rng chi(X,C) c= {0,1} by FUNCT_3:48; hence thesis by A1,A2,TARSKI:def 2; end; assume that A3: chi(X,C).c = 0 and A4: chi(X,C).c = 1; thus contradiction by A3,A4; end; theorem X misses Y implies chi(X,C) + chi(Y,C) = chi(X \/ Y,C) proof assume A1: X /\ Y = {}; A2: dom (chi(X,C) + chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by SEQ_1:def 3 .= C /\ dom chi(Y,C) by Th77 .= C /\ C by Th77 .= dom chi(X \/ Y,C) by Th77; now let c such that A3: c in dom (chi(X,C) + chi(Y,C)); now per cases; suppose A4: c in X; then A5: chi(X,C).c = 1 by Th77; not c in Y by A1,A4,XBOOLE_0:def 3; then A6: chi(Y,C).c = 0 by Th77; c in X \/ Y by A4,XBOOLE_0:def 2; hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A5,A6,Th77; suppose A7: not c in X; then A8: chi(X,C).c = 0 by Th77; now per cases; suppose A9: c in Y; then A10: chi(Y,C).c = 1 by Th77; c in X \/ Y by A9,XBOOLE_0:def 2; hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A10,Th77; suppose A11: not c in Y; then A12: chi(Y,C).c = 0 by Th77; not c in X \/ Y by A7,A11,XBOOLE_0:def 2; hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A12,Th77; end; hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c; end; hence (chi(X,C) + chi(Y,C)).c = chi(X \/ Y,C).c by A3,SEQ_1:def 3; end; hence thesis by A2,PARTFUN1:34; end; theorem chi(X,C) (#) chi(Y,C) = chi(X /\ Y,C) proof A1: dom (chi(X,C) (#) chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by SEQ_1:def 5 .= C /\ dom chi(Y,C) by Th77 .= C /\ C by Th77 .= dom chi(X /\ Y,C) by Th77; now let c such that A2: c in dom (chi(X,C) (#) chi(Y,C)); now per cases; suppose A3: chi(X,C).c * chi(Y,C).c = 0; now per cases by A3,XCMPLX_1:6; suppose chi(X,C).c = 0; then not c in X by Th77; then not c in X /\ Y by XBOOLE_0:def 3; hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A3,Th77; suppose chi(Y,C).c = 0; then not c in Y by Th77; then not c in X /\ Y by XBOOLE_0:def 3; hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A3,Th77; end; hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c; suppose chi(X,C).c * chi(Y,C).c <> 0; then A4: chi(X,C).c <> 0 & chi(Y,C).c <> 0; then A5: chi(X,C).c = 1 & chi(Y,C).c = 1 by Th84; c in X & c in Y by A4,Th77; then c in X /\ Y by XBOOLE_0:def 3; hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A5,Th77; end; hence (chi(X,C)(#)chi(Y,C)).c = chi(X /\ Y,C).c by A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; :: :: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL :: definition let C; let f,Y; pred f is_bounded_above_on Y means :Def9: ex r st for c st c in Y /\ dom f holds f.c <= r; pred f is_bounded_below_on Y means :Def10: ex r st for c st c in Y /\ dom f holds r <= f.c; end; definition let C; let f,Y; pred f is_bounded_on Y means :Def11: f is_bounded_above_on Y & f is_bounded_below_on Y; end; canceled 3; theorem Th90: f is_bounded_on Y iff ex r st for c st c in Y /\ dom f holds abs(f.c)<=r proof thus f is_bounded_on Y implies ex r st for c st c in Y /\ dom f holds abs(f.c)<=r proof assume A1: f is_bounded_on Y; then f is_bounded_above_on Y by Def11; then consider r1 such that A2: for c st c in Y /\ dom f holds f.c <= r1 by Def9; f is_bounded_below_on Y by A1,Def11; then consider r2 such that A3: for c st c in Y /\ dom f holds r2 <= f.c by Def10; take g=abs(r1)+abs(r2); let c such that A4: c in Y /\ dom f; A5: 0 <= abs(r1) by ABSVALUE:5; A6: 0 <= abs(r2) by ABSVALUE:5; A7: r1 <= abs(r1) by ABSVALUE:11; f.c <= r1 by A2,A4; then f.c <= abs(r1) by A7,AXIOMS:22; then A8: f.c + 0 <= abs(r1)+abs(r2) by A6,REAL_1:55; A9: -abs(r2) <= r2 by ABSVALUE:11; A10: -abs(r1) <= 0 by A5,REAL_1:26,50; r2 <= f.c by A3,A4; then -abs(r2) <= f.c by A9,AXIOMS:22; then A11: -abs(r1)+-abs(r2) <= 0 + f.c by A10,REAL_1:55; -abs(r1)+-abs(r2) = -abs(r1)+-(1*abs(r2)) .= -(1*abs(r1)) + (-1)*abs(r2) by XCMPLX_1:175 .= (-1)*abs(r1) + (-1)*abs(r2) by XCMPLX_1:175 .= (-1)*g by XCMPLX_1:8 .= -(1*g) by XCMPLX_1:175 .= -g; hence abs(f.c) <= g by A8,A11,ABSVALUE:12; end; given r such that A12: for c st c in Y /\ dom f holds abs(f.c) <= r; now let c; assume c in Y /\ dom f; then A13: abs(f.c) <= r by A12; f.c <= abs(f.c) by ABSVALUE:11; hence f.c <= r by A13,AXIOMS:22; end; then A14: f is_bounded_above_on Y by Def9; now let c; assume c in Y /\ dom f; then abs(f.c) <= r by A12; then A15: -r <= -abs(f.c) by REAL_1:50; -abs(f.c) <= f.c by ABSVALUE:11; hence -r <= f.c by A15,AXIOMS:22; end; then f is_bounded_below_on Y by Def10; hence thesis by A14,Def11; end; theorem (Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y) & (Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y) & (Y c= X & f is_bounded_on X implies f is_bounded_on Y) proof thus A1: (Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y) proof assume A2: Y c= X & f is_bounded_above_on X; then consider r such that A3: for c st c in X /\ dom f holds f.c <= r by Def9; take r; let c; assume c in Y /\ dom f; then c in Y & c in dom f by XBOOLE_0:def 3; then c in X /\ dom f by A2,XBOOLE_0:def 3; hence thesis by A3; end; thus A4: (Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y) proof assume A5: Y c= X & f is_bounded_below_on X; then consider r such that A6: for c st c in X /\ dom f holds r <= f.c by Def10; take r; let c; assume c in Y /\ dom f; then c in Y & c in dom f by XBOOLE_0:def 3; then c in X /\ dom f by A5,XBOOLE_0:def 3; hence thesis by A6; end; assume Y c= X & f is_bounded_on X; hence thesis by A1,A4,Def11; end; theorem f is_bounded_above_on X & f is_bounded_below_on Y implies f is_bounded_on X /\ Y proof assume A1: f is_bounded_above_on X & f is_bounded_below_on Y; then consider r1 such that A2: for c st c in X /\ dom f holds f.c <= r1 by Def9; consider r2 such that A3: for c st c in Y /\ dom f holds r2 <= f.c by A1,Def10; now let c; assume c in X /\ Y /\ dom f; then c in X /\ Y & c in dom f by XBOOLE_0:def 3; then c in X & c in dom f by XBOOLE_0:def 3; then c in X /\ dom f by XBOOLE_0:def 3; hence f.c <= r1 by A2; end; hence f is_bounded_above_on X /\ Y by Def9; now let c; assume c in X /\ Y /\ dom f; then c in X /\ Y & c in dom f by XBOOLE_0:def 3; then c in Y & c in dom f by XBOOLE_0:def 3; then c in Y /\ dom f by XBOOLE_0:def 3; hence r2 <= f.c by A3; end; hence thesis by Def10; end; theorem X misses dom f implies f is_bounded_on X proof assume X /\ dom f = {}; then for c holds c in X /\ dom f implies abs(f.c) <= 0; hence thesis by Th90; end; theorem 0 = r implies r(#)f is_bounded_on Y proof assume A1: 0 = r; reconsider p1 = 0 as Real; now take p=p1; let c; assume c in Y /\ dom (r(#)f); then A2: c in dom (r(#)f) by XBOOLE_0:def 3; r*f.c <= 0 by A1; hence (r(#)f).c <= p by A2,SEQ_1:def 6; end; hence r(#)f is_bounded_above_on Y by Def9; take p=p1; let c; assume c in Y /\ dom (r(#)f); then A3: c in dom (r(#)f) by XBOOLE_0:def 3; 0 <= r*f.c by A1; hence p <= (r(#)f).c by A3,SEQ_1:def 6; end; theorem Th95: (f is_bounded_above_on Y & 0<=r implies r(#)f is_bounded_above_on Y) & (f is_bounded_above_on Y & r<=0 implies r(#)f is_bounded_below_on Y) proof thus f is_bounded_above_on Y & 0<=r implies r(#)f is_bounded_above_on Y proof assume A1: f is_bounded_above_on Y & 0<=r; then consider r1 such that A2: for c st c in Y /\ dom f holds f.c <= r1 by Def9; take p = r*abs(r1); let c; assume c in Y /\ dom (r(#)f); then A3: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3; then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def 3; then A4: f.c <= r1 by A2; r1 <= abs(r1) by ABSVALUE:11; then f.c <= abs(r1) by A4,AXIOMS:22; then r * (f.c) <= abs(r1)*r by A1,AXIOMS:25; hence (r(#)f).c <= p by A3,SEQ_1:def 6; end; assume A5: f is_bounded_above_on Y & r<=0; then consider r1 such that A6: for c st c in Y /\ dom f holds f.c <= r1 by Def9; take p=r*abs(r1); let c; assume c in Y /\ dom (r(#)f); then A7: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3; then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def 3; then A8: f.c <= r1 by A6; r1<=abs(r1) by ABSVALUE:11; then f.c <= abs(r1) by A8,AXIOMS:22; then p <= r * f.c by A5,REAL_1:52; hence p <= (r(#)f).c by A7,SEQ_1:def 6; end; theorem Th96: (f is_bounded_below_on Y & 0<=r implies r(#)f is_bounded_below_on Y) & (f is_bounded_below_on Y & r<=0 implies r(#)f is_bounded_above_on Y) proof thus f is_bounded_below_on Y & 0<=r implies r(#)f is_bounded_below_on Y proof assume A1: f is_bounded_below_on Y & 0<=r; then consider r1 such that A2: for c st c in Y /\ dom f holds r1 <= f.c by Def10; take p = r*r1; let c; assume c in Y /\ dom (r(#)f); then A3: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3; then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def 3 ; then r1 <= f.c by A2; then p <= (f.c)*r by A1,AXIOMS:25; hence p <= (r(#)f).c by A3,SEQ_1:def 6; end; assume A4: f is_bounded_below_on Y & r<=0; then consider r1 such that A5: for c st c in Y /\ dom f holds r1 <= f.c by Def10; take p=r*(-abs(r1)); let c; assume c in Y /\ dom (r(#)f); then A6: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3; then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def 3 ; then A7: r1 <= f.c by A5; -abs(r1) <= r1 by ABSVALUE:11; then -abs(r1) <= f.c by A7,AXIOMS:22; then r * f.c <= p by A4,REAL_1:52; hence (r(#)f).c <= p by A6,SEQ_1:def 6; end; theorem Th97: f is_bounded_on Y implies r(#)f is_bounded_on Y proof assume f is_bounded_on Y; then A1: f is_bounded_above_on Y & f is_bounded_below_on Y by Def11; now per cases; suppose A2: 0 <= r; hence r(#)f is_bounded_above_on Y by A1,Th95; thus r(#)f is_bounded_below_on Y by A1,A2,Th96; suppose A3: r <= 0; hence r(#)f is_bounded_above_on Y by A1,Th96; thus r(#)f is_bounded_below_on Y by A1,A3,Th95; end; hence r(#)f is_bounded_on Y by Def11; end; theorem abs(f) is_bounded_below_on X proof consider p such that A1: p=0; take p; let c; assume c in X /\ dom (abs(f)); then A2: c in dom (abs(f)) by XBOOLE_0:def 3; 0 <= abs( f.c ) by ABSVALUE:5; hence p <= (abs(f)).c by A1,A2,SEQ_1:def 10; end; theorem Th99: f is_bounded_on Y implies abs(f) is_bounded_on Y & -f is_bounded_on Y proof assume A1: f is_bounded_on Y; then consider r1 such that A2: for c st c in Y /\ dom f holds abs(f.c) <= r1 by Th90; now let c; assume c in Y /\ dom (abs(f)); then A3: c in Y & c in dom (abs(f)) by XBOOLE_0:def 3 ; then c in Y & c in dom f by SEQ_1:def 10; then c in Y /\ dom f by XBOOLE_0:def 3; then abs(abs(f.c)) <= r1 by A2; hence abs((abs(f)).c) <= r1 by A3,SEQ_1:def 10; end; hence abs(f) is_bounded_on Y by Th90; (-1)(#)f is_bounded_on Y by A1,Th97; hence thesis by Th38; end; theorem Th100: (f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies f1+f2 is_bounded_above_on (X /\ Y)) & (f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies f1+f2 is_bounded_below_on (X /\ Y)) & (f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y)) proof thus A1: f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies f1+f2 is_bounded_above_on (X /\ Y) proof assume A2: f1 is_bounded_above_on X & f2 is_bounded_above_on Y; then consider r1 such that A3: for c st c in X /\ dom f1 holds f1.c <= r1 by Def9; consider r2 such that A4: for c st c in Y /\ dom f2 holds f2.c <= r2 by A2,Def9; take r=r1+r2; let c; assume c in X /\ Y /\ dom (f1+f2); then A5: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 3,XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A6: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; then A7: f1.c <= r1 by A3; f2.c <= r2 by A4,A6; then f1.c + f2.c <= r by A7,REAL_1:55; hence (f1+f2).c <= r by A5,SEQ_1:def 3; end; thus A8: f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies f1+f2 is_bounded_below_on (X /\ Y) proof assume A9: f1 is_bounded_below_on X & f2 is_bounded_below_on Y; then consider r1 such that A10: for c st c in X /\ dom f1 holds r1 <= f1.c by Def10; consider r2 such that A11: for c st c in Y /\ dom f2 holds r2 <= f2.c by A9,Def10; take r=r1+r2; let c; assume c in X /\ Y /\ dom (f1+f2); then A12: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 3,XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A13: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; then A14: r1 <= f1.c by A10; r2 <= f2.c by A11,A13; then r <= f1.c + f2.c by A14,REAL_1:55; hence r <= (f1+f2).c by A12,SEQ_1:def 3; end; assume A15: f1 is_bounded_on X & f2 is_bounded_on Y; hence f1+f2 is_bounded_above_on (X /\ Y) by A1,Def11; thus f1+f2 is_bounded_below_on (X /\ Y) by A8,A15,Def11; end; theorem Th101: f1 is_bounded_on X & f2 is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y) & f1-f2 is_bounded_on X /\ Y proof assume A1: f1 is_bounded_on X & f2 is_bounded_on Y; then consider r1 such that A2: for c st c in X /\ dom f1 holds abs(f1.c) <= r1 by Th90; consider r2 such that A3: for c st c in Y /\ dom f2 holds abs(f2.c) <= r2 by A1,Th90; now take r=r1*r2; let c; assume c in X /\ Y /\ dom (f1(#)f2); then A4: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 5,XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A5: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; then A6: abs(f1.c) <= r1 by A2; A7: abs(f2.c) <= r2 by A3,A5; A8: 0<=abs(f1.c) by ABSVALUE:5; 0<=abs(f2.c) by ABSVALUE:5; then abs(f1.c)*abs(f2.c) <= r by A6,A7,A8,Th2; then abs(f1.c * f2.c) <= r by ABSVALUE:10; hence abs((f1(#)f2).c) <= r by A4,SEQ_1:def 5; end; hence f1(#)f2 is_bounded_on X /\ Y by Th90; -f2 is_bounded_on Y by A1,Th99; then f1+-f2 is_bounded_on (X /\ Y) by A1, Th100; hence thesis by Th40; end; theorem Th102: f is_bounded_above_on X & f is_bounded_above_on Y implies f is_bounded_above_on X \/ Y proof assume A1: f is_bounded_above_on X & f is_bounded_above_on Y; then consider r1 such that A2: for c st c in X /\ dom f holds f.c <= r1 by Def9; consider r2 such that A3: for c st c in Y /\ dom f holds f.c <= r2 by A1,Def9; take r = abs(r1) + abs(r2); let c; assume c in (X \/ Y) /\ dom f; then A4: c in X \/ Y & c in dom f by XBOOLE_0:def 3; now per cases by A4,XBOOLE_0:def 2; suppose c in X; then c in X /\ dom f by A4,XBOOLE_0:def 3 ; then A5: f.c <= r1 by A2; r1 <= abs(r1) by ABSVALUE:11; then A6: f.c <= abs(r1) by A5,AXIOMS:22; 0 <= abs(r2) by ABSVALUE:5; then f.c + 0 <= r by A6,REAL_1:55; hence f.c <= r; suppose c in Y; then c in Y /\ dom f by A4,XBOOLE_0:def 3 ; then A7: f.c <= r2 by A3; r2 <= abs(r2) by ABSVALUE:11; then A8: f.c <= abs(r2) by A7,AXIOMS:22; 0 <= abs(r1) by ABSVALUE:5; then 0 + f.c <= r by A8,REAL_1:55; hence f.c <= r; end; hence f.c <= r; end; theorem Th103: f is_bounded_below_on X & f is_bounded_below_on Y implies f is_bounded_below_on X \/ Y proof assume A1: f is_bounded_below_on X & f is_bounded_below_on Y; then consider r1 such that A2: for c st c in X /\ dom f holds r1 <= f.c by Def10; consider r2 such that A3: for c st c in Y /\ dom f holds r2 <= f.c by A1,Def10; take r = -abs(r1) - abs(r2); let c; assume c in (X \/ Y) /\ dom f; then A4: c in X \/ Y & c in dom f by XBOOLE_0:def 3; now per cases by A4,XBOOLE_0:def 2; suppose c in X; then c in X /\ dom f by A4,XBOOLE_0:def 3 ; then A5: r1 <= f.c by A2; -abs(r1) <= r1 by ABSVALUE:11; then A6: -abs(r1) <= f.c by A5,AXIOMS:22; 0 <= abs(r2) by ABSVALUE:5; then r <= f.c - 0 by A6,REAL_1:92; hence r <= f.c; suppose c in Y; then c in Y /\ dom f by A4,XBOOLE_0:def 3; then A7: r2 <= f.c by A3; -abs(r2) <= r2 by ABSVALUE:11; then A8: -abs(r2) <= f.c by A7,AXIOMS:22; 0 <= abs(r1) by ABSVALUE:5; then -abs(r2) - abs(r1) <= f.c - 0 by A8,REAL_1:92; then -abs(r1) +- abs(r2) <= f.c - 0 by XCMPLX_0:def 8; hence r <= f.c by XCMPLX_0:def 8; end; hence r <= f.c; end; theorem f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y proof assume A1: f is_bounded_on X & f is_bounded_on Y; then A2: f is_bounded_above_on X & f is_bounded_below_on X by Def11; A3: f is_bounded_above_on Y & f is_bounded_below_on Y by A1,Def11; hence f is_bounded_above_on X \/ Y by A2,Th102; thus f is_bounded_below_on X \/ Y by A2,A3,Th103; end; theorem f1 is_constant_on X & f2 is_constant_on Y implies (f1 + f2) is_constant_on (X /\ Y) & (f1 - f2) is_constant_on (X /\ Y) & (f1 (#) f2) is_constant_on (X /\ Y) proof assume A1: f1 is_constant_on X & f2 is_constant_on Y; then consider r1 be Real such that A2: for c st c in X /\ dom f1 holds f1.c = r1 by PARTFUN2:76; consider r2 be Real such that A3: for c st c in Y /\ dom f2 holds f2.c = r2 by A1,PARTFUN2:76; now let c; assume c in X /\ Y /\ dom (f1+f2); then A4: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3; then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 3,XBOOLE_0:def 3 ; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A5: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; thus (f1+f2).c =f1.c + f2.c by A4,SEQ_1:def 3 .= r1 + f2.c by A2,A5 .= r1 + r2 by A3,A5; end; hence (f1 + f2) is_constant_on (X /\ Y) by PARTFUN2:76; now let c; assume c in X /\ Y /\ dom (f1-f2); then A6: c in X /\ Y & c in dom (f1-f2) by XBOOLE_0:def 3; then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 4,XBOOLE_0:def 3 ; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A7: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; thus (f1-f2).c = f1.c - f2.c by A6,SEQ_1:def 4 .= r1 - f2.c by A2,A7 .= r1 - r2 by A3,A7; end; hence (f1 - f2) is_constant_on (X /\ Y) by PARTFUN2:76; now let c; assume c in X /\ Y /\ dom (f1(#)f2); then A8: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3; then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 5,XBOOLE_0:def 3 ; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A9: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; thus (f1(#)f2).c =f1.c * f2.c by A8,SEQ_1:def 5 .= r1 * f2.c by A2,A9 .= r1 * r2 by A3,A9; end; hence thesis by PARTFUN2:76; end; theorem Th106: f is_constant_on Y implies p(#)f is_constant_on Y proof assume f is_constant_on Y; then consider r be Real such that A1: for c be Element of C st c in Y /\ dom f holds f.c = r by PARTFUN2:76; reconsider p as Real by XREAL_0:def 1; now let c; assume c in Y /\ dom (p(#)f); then A2: c in dom (p(#)f) & c in Y by XBOOLE_0:def 3; then c in dom f by SEQ_1:def 6; then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3; thus (p(#)f).c = p * f.c by A2,SEQ_1:def 6 .= p*r by A1,A3; end; hence thesis by PARTFUN2:76; end; theorem Th107: f is_constant_on Y implies abs(f) is_constant_on Y & -f is_constant_on Y proof assume f is_constant_on Y; then consider r be Real such that A1: for c st c in Y /\ dom f holds f.c = r by PARTFUN2:76; now let c; assume c in Y /\ dom (abs(f)); then A2: c in dom (abs(f)) & c in Y by XBOOLE_0:def 3; then c in dom f by SEQ_1:def 10; then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3; thus (abs(f)).c = abs(f.c) by A2,SEQ_1:def 10 .= abs(r) by A1,A3; end; hence abs(f) is_constant_on Y by PARTFUN2:76; now take p=-r; let c; assume A4: c in Y /\ dom (-f); then c in Y /\ dom f by SEQ_1:def 7; then A5: -f.c = p by A1; c in dom (-f) by A4,XBOOLE_0:def 3; hence (-f).c = p by A5,SEQ_1:def 7; end; hence thesis by PARTFUN2:76; end; theorem Th108: f is_constant_on Y implies f is_bounded_on Y proof assume f is_constant_on Y; then consider r be Real such that A1: for c st c in Y /\ dom f holds f.c = r by PARTFUN2:76; now take p=abs(r); let c; assume c in Y /\ dom f; hence abs(f.c) <= p by A1; end; hence thesis by Th90; end; theorem f is_constant_on Y implies (for r holds r(#)f is_bounded_on Y) & (-f is_bounded_on Y) & abs(f) is_bounded_on Y proof assume A1: f is_constant_on Y; now let r; r(#)f is_constant_on Y by A1,Th106; hence r(#)f is_bounded_on Y by Th108; end; hence for r holds r(#)f is_bounded_on Y; -f is_constant_on Y by A1,Th107; hence -f is_bounded_on Y by Th108; abs(f) is_constant_on Y by A1,Th107; hence thesis by Th108; end; theorem Th110: (f1 is_bounded_above_on X & f2 is_constant_on Y implies f1+f2 is_bounded_above_on (X /\ Y)) & (f1 is_bounded_below_on X & f2 is_constant_on Y implies f1+f2 is_bounded_below_on (X /\ Y)) & (f1 is_bounded_on X & f2 is_constant_on Y implies f1+f2 is_bounded_on (X /\ Y)) proof thus f1 is_bounded_above_on X & f2 is_constant_on Y implies f1+f2 is_bounded_above_on (X /\ Y) proof assume A1: f1 is_bounded_above_on X & f2 is_constant_on Y; then f2 is_bounded_on Y by Th108; then f2 is_bounded_above_on Y by Def11; hence thesis by A1,Th100; end; thus f1 is_bounded_below_on X & f2 is_constant_on Y implies f1+f2 is_bounded_below_on (X /\ Y) proof assume A2: f1 is_bounded_below_on X & f2 is_constant_on Y; then f2 is_bounded_on Y by Th108; then f2 is_bounded_below_on Y by Def11; hence thesis by A2,Th100; end; assume A3: f1 is_bounded_on X & f2 is_constant_on Y; then f2 is_bounded_on Y by Th108; hence thesis by A3,Th100; end; theorem (f1 is_bounded_above_on X & f2 is_constant_on Y implies f1-f2 is_bounded_above_on (X /\ Y)) & (f1 is_bounded_below_on X & f2 is_constant_on Y implies f1-f2 is_bounded_below_on X /\ Y) & (f1 is_bounded_on X & f2 is_constant_on Y implies f1-f2 is_bounded_on X /\ Y & f2-f1 is_bounded_on X /\ Y & f1(#)f2 is_bounded_on X /\ Y) proof thus f1 is_bounded_above_on X & f2 is_constant_on Y implies f1-f2 is_bounded_above_on X /\ Y proof assume A1: f1 is_bounded_above_on X & f2 is_constant_on Y; then -f2 is_constant_on Y by Th107; then f1+-f2 is_bounded_above_on X /\ Y by A1,Th110; hence thesis by Th40; end; thus f1 is_bounded_below_on X & f2 is_constant_on Y implies f1-f2 is_bounded_below_on X /\ Y proof assume A2: f1 is_bounded_below_on X & f2 is_constant_on Y; then -f2 is_constant_on Y by Th107; then f1+-f2 is_bounded_below_on X /\ Y by A2,Th110; hence thesis by Th40; end; assume A3: f1 is_bounded_on X & f2 is_constant_on Y; then -f2 is_constant_on Y by Th107; then f1+-f2 is_bounded_on X /\ Y by A3,Th110; hence f1-f2 is_bounded_on X /\ Y by Th40; A4: f2 is_bounded_on Y by A3,Th108; hence f2-f1 is_bounded_on X /\ Y by A3,Th101; thus thesis by A3,A4,Th101; end;

Back to top