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