CFUNCT_1

:: Property of Complex Functions
::  by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, PARTFUN1, NUMBERS, RELAT_1, ARYTM_3, CARD_1,
      COMPLEX1, ORDINAL4, FUNCT_1, ARYTM_1, VALUED_1, TARSKI, XXREAL_2,
      XXREAL_0, FUNCT_7, REAL_1, XCMPLX_0, VALUED_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RFUNCT_1,
      COMPLEX1, VALUED_0, VALUED_1, COMSEQ_2, SEQ_2;
 constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, VALUED_1,
      RFUNCT_1, SEQ_2, NAT_1, RELSET_1, COMSEQ_2;
 registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RFUNCT_1,
      XCMPLX_0, VALUED_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, COMSEQ_2;
 equalities XBOOLE_0, VALUED_1;
 expansions PARTFUN1, XBOOLE_0, COMSEQ_2, VALUED_1;
 theorems TARSKI, SUBSET_1, FUNCT_1, PARTFUN1, PARTFUN2, RFUNCT_1, COMPLEX1,
      RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0,
      VALUED_1, XREAL_0, FUNCT_2;
 schemes PARTFUN2;

begin

reserve x,y,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,COMPLEX;
reserve r1,r2,p1 for Real;
reserve r,q,cr1,cr2 for Complex;

::
::DEFINITIONS OF COMPLEX FUNCTIONS
::

definition
  let C,f1,f2;
  deffunc F(set) = f1/.$1 * (f2/.$1)";
  func f1/f2 -> PartFunc of C,COMPLEX means
  :Def1:
  dom it = dom f1 /\ (dom f2 \ f2"{0}) &
    for c st c in dom it holds it/.c = f1/.c * (f2/.c)";
  existence
  proof
    deffunc F(set) = In(f1/.$1 * (f2/.$1)",COMPLEX);
    defpred P[set] means $1 in dom f1 /\ (dom f2 \ f2"{0c});
    consider F being PartFunc of C,COMPLEX 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 = F(c) from PARTFUN2:sch 2;
    take F;
    thus dom F = dom f1 /\ (dom f2 \ f2"{0}) by A1,SUBSET_1:3;
    let c;
    assume c in dom F;
     then F/.c = F(c) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    set X = dom f1 /\ (dom f2 \ f2"{0});
    let f,g be PartFunc of C,COMPLEX such that
A3: dom f=X and
A4: for c be Element of C st c in dom f holds f/.c = F(c) and
A5: dom g=X and
A6: for c be Element of C st c in dom g holds g/.c = F(c);
    now let c be Element of C;
     assume
A7:    c in dom f;
     hence f/.c = F(c) by A4 .= g/.c by A7,A3,A5,A6;
    end;
   hence f = g by A3,A5,PARTFUN2:1;
  end;
end;

definition
  let C,f;
  deffunc F(set) = (f/.$1)";
  func f^ -> PartFunc of C,COMPLEX means
  :Def2:
  dom it = dom f \ f"{0} & for c st c in dom it holds it/.c = (f/.c)";
  existence
  proof
    deffunc F(set) = In((f/.$1)",COMPLEX);
    defpred P[set] means $1 in dom f \ f"{0c};
    consider F being PartFunc of C,COMPLEX 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 = F(c) from PARTFUN2:sch 2;
    take F;
    thus dom F = dom f \ f"{0} by A1,SUBSET_1:3;
    let c;
    assume c in dom F;
     then F/.c = F(c) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    set X = dom f \ f"{0};
   let f1,g1 be PartFunc of C,COMPLEX such that
A3: dom f1=X and
A4: for c be Element of C st c in dom f1 holds f1/.c = F(c) and
A5: dom g1=X and
A6: for c be Element of C st c in dom g1 holds g1/.c = F(c);
    now let c be Element of C;
     assume
A7:    c in dom f1;
     hence f1/.c = F(c) by A4 .= g1/.c by A7,A3,A5,A6;
    end;
   hence f1 = g1 by A3,A5,PARTFUN2:1;
  end;
end;

theorem Th1:
  dom (f1+f2) = dom f1 /\ dom f2 & for c st c in dom(f1+f2) holds
  (f1+f2)/.c = (f1/.c) + (f2/.c)
proof
  thus
A1: dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
  now
    let c;
    assume
A2: c in dom (f1+f2);
    then c in dom f1 by A1,XBOOLE_0:def 4;
    then
A3: f1.c = f1/.c by PARTFUN1:def 6;
    c in dom f2 by A1,A2,XBOOLE_0:def 4;
    then
A4: f2.c = f2/.c by PARTFUN1:def 6;
    thus (f1+f2)/.c = (f1+f2).c by A2,PARTFUN1:def 6
      .= f1/.c+f2/.c by A2,A3,A4,VALUED_1:def 1;
  end;
  hence thesis;
end;

theorem Th2:
  dom (f1-f2) = dom f1 /\ dom f2 & for c st c in dom(f1-f2) holds
  (f1-f2)/.c = (f1/.c) - (f2/.c)
proof
A1: dom (f1-f2) = dom f1 /\ dom(-f2) by VALUED_1:def 1;
  hence dom (f1-f2) = dom f1 /\ dom f2 by VALUED_1:8;
  now
    let c;
    assume
A2: c in dom (f1-f2);
    then
A3: dom -f2 = dom f2 & c in dom -f2 by A1,VALUED_1:8,XBOOLE_0:def 4;
    c in dom f1 by A1,A2,XBOOLE_0:def 4;
    then
A4: f1/.c = f1.c by PARTFUN1:def 6;
    thus (f1-f2)/.c = (f1-f2).c by A2,PARTFUN1:def 6
      .= f1.c - f2.c by A2,VALUED_1:13
      .= f1/.c - f2/.c by A3,A4,PARTFUN1:def 6;
  end;
  hence thesis;
end;

theorem Th3:
  dom(f1(#)f2)=dom f1 /\ dom f2 & for c st c in dom(f1(#)f2) holds
  (f1(#)f2)/.c =(f1/.c) * (f2/.c)
proof
  thus
A1: dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
  now
    let c;
    assume
A2: c in dom (f1(#)f2);
    then c in dom f1 by A1,XBOOLE_0:def 4;
    then
A3: f1.c = f1/.c by PARTFUN1:def 6;
    c in dom f2 by A1,A2,XBOOLE_0:def 4;
    then
A4: f2.c = f2/.c by PARTFUN1:def 6;
    thus (f1(#)f2)/.c = (f1(#)f2).c by A2,PARTFUN1:def 6
      .= f1/.c * f2/.c by A2,A3,A4,VALUED_1:def 4;
  end;
  hence thesis;
end;

theorem Th4:
  dom (r(#)f) = dom f &
  for c st c in dom (r(#)f) holds (r(#)f)/.c = r * (f/.c)
proof
  thus
A1: dom (r(#)f) = dom f by VALUED_1:def 5;
  now
    let c;
    assume
A2: c in dom (r(#)f);
    hence (r(#)f)/.c = (r(#)f).c by PARTFUN1:def 6
      .= r *(f.c) by VALUED_1:6
      .= r *(f/.c) by A1,A2,PARTFUN1:def 6;
  end;
  hence thesis;
end;

theorem Th5:
  dom (-f) = dom f & for c st c in dom (-f) holds (-f)/.c = -f/.c
proof
  thus
A1: dom (-f) = dom f by VALUED_1:8;
  now
    let c;
    assume
A2: c in dom (-f);
    hence (-f)/.c = (-f).c by PARTFUN1:def 6
      .=-f.c by VALUED_1:8
      .=-f/.c by A1,A2,PARTFUN1:def 6;
  end;
  hence thesis;
end;

Lm1: x in f"Y iff x in dom f & f/.x in Y by PARTFUN2:26;

theorem Th6:
  dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0}
proof
  dom (g^) = dom g \ g"{0c} by Def2;
  hence dom (g^) c= dom g by XBOOLE_1:36;
  thus thesis by XBOOLE_1:28,36;
end;

theorem Th7:
  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 be object;
    assume
A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0};
    then
A2: x in dom (f1(#)f2) by XBOOLE_0:def 5;
    reconsider x1=x as Element of C by A1;
    not x in (f1(#)f2)"{0c} by A1,XBOOLE_0:def 5;
    then not (f1(#)f2)/.x1 in {0c} by A2,PARTFUN2:26;
    then (f1(#)f2)/.x1 <> 0c by TARSKI:def 1;
    then
A3: (f1/.x1) * (f2/.x1) <> 0c by A2,Th3;
    then (f2/.x1) <> 0c;
    then not (f2/.x1) in {0c } by TARSKI:def 1;
    then
A4: not x1 in (f2)"{0c} by PARTFUN2:26;
A5: x1 in dom f1 /\ dom f2 by A2,Th3;
    then x1 in dom f2 by XBOOLE_0:def 4;
    then
A6: x in dom f2 \ (f2)"{0c} by A4,XBOOLE_0:def 5;
    (f1/.x1) <> 0c by A3;
    then not (f1/.x1) in {0c} by TARSKI:def 1;
    then
A7: not x1 in (f1)"{0c} by PARTFUN2:26;
    x1 in dom f1 by A5,XBOOLE_0:def 4;
    then x in dom f1 \ (f1)"{0c} by A7,XBOOLE_0:def 5;
    hence thesis by A6,XBOOLE_0:def 4;
  end;
  thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) c= dom (f1(#)f2) \ (f1(#)f2)
  "{0}
  proof
    let x be object;
    assume
A8: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});
    then reconsider x1=x as Element of C;
A9: x in dom f2 \ (f2)"{0c} by A8,XBOOLE_0:def 4;
    then
A10: x in dom f2 by XBOOLE_0:def 5;
    not x in (f2)"{0c } by A9,XBOOLE_0:def 5;
    then not (f2/.x1) in {0c} by A10,PARTFUN2:26;
    then
A11: (f2/.x1) <> 0c by TARSKI:def 1;
A12: x in dom f1 \ (f1)"{0c} by A8,XBOOLE_0:def 4;
    then
A13: x in dom f1 by XBOOLE_0:def 5;
    then x1 in dom f1 /\ dom f2 by A10,XBOOLE_0:def 4;
    then
A14: x1 in dom (f1(#)f2) by Th3;
    not x in (f1)"{0c} by A12,XBOOLE_0:def 5;
    then not (f1/.x1) in {0c} by A13,PARTFUN2:26;
    then (f1/.x1) <> 0c by TARSKI:def 1;
    then (f1/.x1) * (f2/.x1) <>0c by A11,XCMPLX_1:6;
    then (f1(#)f2)/.x1 <> 0c by A14,Th3;
    then not (f1(#)f2)/.x1 in {0c} by TARSKI:def 1;
    then not x in (f1(#)f2)"{0c} by PARTFUN2:26;
    hence thesis by A14,XBOOLE_0:def 5;
  end;
end;

theorem Th8:
  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"{0c} by A1,Def2;
  then
A4: not c in f"{0c} by XBOOLE_0:def 5;
  now
    per cases by A4,PARTFUN2:26;
    suppose
      not c in dom f;
      hence contradiction by A3,XBOOLE_0:def 5;
    end;
    suppose
      not (f/.c) in {0c};
      hence contradiction by A2,TARSKI:def 1;
    end;
  end;
  hence contradiction;
end;

theorem Th9:
  (f^)"{0} = {}
proof
  set x = the Element of (f^)"{0c};
  assume
A1: (f^)"{0} <> {};
  then
A2: x in dom (f^) by Lm1;
A3: (f^)/.x in {0c} by A1,Lm1;
  reconsider x as Element of C by A2;
  x in dom f \ f"{0c} by A2,Def2;
  then x in dom f & not x in f"{0c} by XBOOLE_0:def 5;
  then
A4: not f/.x in {0c} by PARTFUN2:26;
  (f^)/.x = 0c by A3,TARSKI:def 1;
  then (f/.x)" = 0c by A2,Def2;
  hence contradiction by A4,TARSKI:def 1,XCMPLX_1:202;
end;

theorem Th10:
  |.f.|"{0} = f"{0} & (-f)"{0} = f"{0}
proof
A1: dom |.f.| = dom f by VALUED_1:def 11;
  now
    let c;
    thus c in (|.f.|)"{0} implies c in f"{0c}
    proof
      assume
A2:   c in (|.f.|)"{0};
      then c in dom (|.f.|) by FUNCT_1:def 7;
      then
A3:   c in dom f by VALUED_1:def 11;
      (|.f.|).c in {0} by A2,FUNCT_1:def 7;
      then (|.f.|).c = 0 by TARSKI:def 1;
      then
A4:   |.(f.c).| = 0 by VALUED_1:18;
      c in dom (|.f.|) by A2,FUNCT_1:def 7;
      then f.c = f/.c by A1,PARTFUN1:def 6;
      then (f/.c) = 0c by A4,COMPLEX1:45;
      then (f/.c) in {0c} by TARSKI:def 1;
      hence thesis by A3,PARTFUN2:26;
    end;
    assume
A5: c in (f)"{0c};
    then (f/.c) in {0c} by PARTFUN2:26;
    then
A6: |.(f/.c).| = 0 by COMPLEX1:44,TARSKI:def 1;
A7: c in dom f by A5,PARTFUN2:26;
    then f.c = f/.c by PARTFUN1:def 6;
    then (|.f.|).c = 0 by A6,VALUED_1:18;
    then
A8: (|.f.|).c in {0} by TARSKI:def 1;
    c in dom (|.f.|) by A7,VALUED_1:def 11;
    hence c in (|.f.|)"{0} by A8,FUNCT_1:def 7;
  end;
  hence (|.f.|)"{0} = f"{0} by SUBSET_1:3;
  now
    let c;
    thus c in (-f)"{0c} implies c in f"{0c}
    proof
      assume
A9:   c in (-f)"{0c};
      then
A10:  c in dom (-f) by PARTFUN2:26;
      (-f)/.c in {0c} by A9,PARTFUN2:26;
      then (-f)/.c = 0c by TARSKI:def 1;
      then --((f/.c)) = -0c by A10,Th5;
      then
A11:  (f/.c) in {0c} by TARSKI:def 1;
      c in dom f by A10,Th5;
      hence thesis by A11,PARTFUN2:26;
    end;
    assume
A12: c in (f)"{0c};
    then (f/.c) in {0c} by PARTFUN2:26;
    then
A13: (f/.c) = 0c by TARSKI:def 1;
A14: c in dom f by A12,PARTFUN2:26;
    then c in dom (-f) by Th5;
    then (-f)/.c = -0c by A13,Th5;
    then
A15: (-f)/.c in {0c} by TARSKI:def 1;
    c in dom (-f) by A14,Th5;
    hence c in (-f)"{0c} by A15,PARTFUN2:26;
  end;
  hence thesis by SUBSET_1:3;
end;

theorem Th11:
  dom (f^^) = dom (f|(dom (f^)))
proof
A1: dom (f^) = dom f \ f"{0c} by Def2;
  thus dom (f^^) = dom (f^) \(f^)"{0c} by Def2
    .= dom (f^) \ {} by Th9
    .= dom f /\ dom (f^) by A1,XBOOLE_1:28,36
    .= dom (f|(dom (f^))) by RELAT_1:61;
end;

theorem Th12:
  r <> 0 implies (r(#)f)"{0} = f"{0}
proof
  assume
A1: r <> 0;
  now
    let c;
    thus c in (r(#)f)"{0c} implies c in f"{0c}
    proof
      assume
A2:   c in (r(#)f)"{0c};
      then
A3:   c in dom (r(#)f) by PARTFUN2:26;
      (r(#)f)/.c in {0c} by A2,PARTFUN2:26;
      then (r(#)f)/.c = 0c by TARSKI:def 1;
      then r*(f/.c) = 0c by A3,Th4;
      then (f/.c) = 0c by A1,XCMPLX_1:6;
      then
A4:   (f/.c) in {0c} by TARSKI:def 1;
      c in dom f by A3,Th4;
      hence thesis by A4,PARTFUN2:26;
    end;
    assume
A5: c in (f)"{0c};
    then (f/.c) in {0c} by PARTFUN2:26;
    then (f/.c) = 0c by TARSKI:def 1;
    then
A6: r*(f/.c) = 0c;
A7: c in dom f by A5,PARTFUN2:26;
    then c in dom (r(#)f) by Th4;
    then (r(#)f)/.c = 0c by A6,Th4;
    then
A8: (r(#)f)/.c in {0c} by TARSKI:def 1;
    c in dom (r(#)f) by A7,Th4;
    hence c in (r(#)f)"{0c} by A8,PARTFUN2:26;
  end;
  hence thesis by SUBSET_1:3;
end;

begin

::
:: BASIC PROPERTIES OF OPERATIONS
::

theorem Tassoc:
  for f1,f2,f3 being complex-valued Function holds
  (f1 + f2) + f3 = f1 + (f2 + f3)
proof
  let f1,f2,f3 be complex-valued Function;
  thus
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by VALUED_1:def 1
    .= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 1
    .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
    .= dom f1 /\ dom (f2 + f3) by VALUED_1:def 1
    .= dom (f1 + (f2 + f3)) by VALUED_1:def 1;
    let c be object;
    assume
A2: c in dom (f1 + f2 + f3);
    then c in dom (f1 + f2) /\ dom f3 by VALUED_1:def 1;
    then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
    c in dom f1 /\ dom (f2 + f3) by A1,A2,VALUED_1:def 1;
    then
A4: c in dom (f2 + f3) by XBOOLE_0:def 4;
    thus (f1 + f2 + f3).c = (f1 + f2).c + (f3.c) by A2,VALUED_1:def 1
    .= ((f1.c)) + ((f2.c)) + (f3.c) by A3,VALUED_1:def 1
    .= ((f1.c)) + (((f2.c)) + (f3.c))
    .= ((f1.c)) + (f2 + f3).c by A4,VALUED_1:def 1
    .= (f1 + (f2 + f3)).c by A1,A2,VALUED_1:def 1;
end;

theorem Th14:
  for f1,f2,f3 being complex-valued Function holds
  (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
  let f1,f2,f3 be complex-valued Function;
  thus
A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by VALUED_1:def 4
    .= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4
    .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
    .= dom f1 /\ dom (f2 (#) f3) by VALUED_1:def 4
    .= dom (f1 (#) (f2 (#) f3)) by VALUED_1:def 4;
    let c be object;
    assume
A2: c in dom (f1(#)f2(#)f3);
    then c in dom (f1 (#) f2) /\ dom f3 by VALUED_1:def 4;
    then
A3: c in dom (f1 (#) f2) by XBOOLE_0:def 4;
    c in dom f1 /\ dom (f2(#)f3) by A1,A2,VALUED_1:def 4;
    then
A4: c in dom (f2 (#) f3) by XBOOLE_0:def 4;
    thus (f1 (#) f2 (#) f3).c = (f1 (#) f2).c * (f3.c) by A2,VALUED_1:def 4
      .= ((f1.c)) * ((f2.c)) * (f3.c) by A3,VALUED_1:def 4
      .= ((f1.c)) * (((f2.c)) * (f3.c))
      .= ((f1.c)) * ((f2 (#) f3).c) by A4,VALUED_1:def 4
      .= (f1 (#) (f2 (#) f3)).c by A1,A2,VALUED_1:def 4;
end;

theorem Th15:
  for f1,f2,f3 being complex-valued Function holds
  (f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3
proof
  let f1,f2,f3 be complex-valued Function;
  thus
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by VALUED_1:def 4
    .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:def 1
    .= 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 VALUED_1:def 4
    .= dom (f1 (#) f3) /\ dom (f2 (#) f3) by VALUED_1:def 4
    .= dom (f1 (#) f3 + f2 (#) f3) by VALUED_1:def 1;
    let c be object;
    assume
A2: c in dom ((f1 + f2)(#)f3);
    then
A3: c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VALUED_1:def 1;
    then
A4: c in dom (f1(#)f3) by XBOOLE_0:def 4;
    c in dom (f1 + f2) /\ dom f3 by A2,VALUED_1:def 4;
    then
A5: c in dom (f1 + f2) by XBOOLE_0:def 4;
A6: c in dom (f2 (#) f3) by A3,XBOOLE_0:def 4;
    thus ((f1 + f2) (#) f3).c = (f1 + f2).c * (f3.c) by A2,VALUED_1:def 4
      .= (((f1.c)) + ((f2.c))) * (f3.c) by A5,VALUED_1:def 1
      .= ((f1.c)) * (f3.c) + ((f2.c)) * (f3.c)
      .= (f1 (#) f3).c + ((f2.c))* (f3.c) by A4,VALUED_1:def 4
      .= (f1 (#) f3).c + (f2 (#) f3).c by A6,VALUED_1:def 4
      .=((f1 (#) f3) + (f2 (#) f3)).c by A1,A2,VALUED_1:def 1;
end;

theorem
  for f1,f2,f3 being complex-valued Function holds
  f3 (#) (f1 + f2) = f3(#)f1 + f3(#)f2 by Th15;

theorem Th17:
  for f1,f2 being complex-valued Function holds r(#)(f1(#)f2) = r(#)f1(#)f2
proof
  let f1,f2 be complex-valued Function;
  thus
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 5
    .= dom f1 /\ dom f2 by VALUED_1:def 4
    .= dom (r(#)f1) /\ dom f2 by VALUED_1:def 5
    .= dom (r(#)f1(#)f2) by VALUED_1:def 4;
    let c be object;
    assume
A2: c in dom (r(#)(f1(#)f2));
    then
A3: c in dom (f1(#)f2) by VALUED_1:def 5;
    c in dom (r(#)f1) /\ dom f2 by A1,A2,VALUED_1:def 4;
    then
A4: c in dom (r(#)f1) by XBOOLE_0:def 4;
    thus (r(#)(f1(#)f2)).c = r * ((f1(#)f2).c) by A2,VALUED_1:def 5
      .= r*(((f1.c)) * ((f2.c))) by A3,VALUED_1:def 4
      .= (r*((f1.c))) * ((f2.c))
      .= (r(#)f1).c * ((f2.c)) by A4,VALUED_1:def 5
      .= (r(#)f1 (#) f2).c by A1,A2,VALUED_1:def 4;
end;

theorem Th18:
  for f1,f2 being complex-valued Function holds r(#)(f1(#)f2) = f1(#)(r(#)f2)
proof
  let f1,f2 be complex-valued Function;
  thus
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 5
    .= dom f1 /\ dom f2 by VALUED_1:def 4
    .= dom f1 /\ dom (r(#)f2) by VALUED_1:def 5
    .= dom (f1(#)(r(#)f2)) by VALUED_1:def 4;
    let c be object;
    assume
A2: c in dom (r(#)(f1(#)f2));
    then
A3: c in dom (f1(#)f2) by VALUED_1:def 5;
    c in dom f1 /\ dom (r(#)f2) by A1,A2,VALUED_1:def 4;
    then
A4: c in dom (r(#)f2) by XBOOLE_0:def 4;
    thus (r(#)(f1(#)f2)).c = r * ((f1(#)f2).c) by A2,VALUED_1:def 5
      .= r * (((f1.c)) * ((f2.c))) by A3,VALUED_1:def 4
      .= ((f1.c)) * (r * ((f2.c)))
      .= ((f1.c)) * ((r(#)f2).c) by A4,VALUED_1:def 5
      .= (f1(#)(r(#)f2)).c by A1,A2,VALUED_1:def 4;
end;

theorem Th19:
  for f1,f2,f3 being complex-valued Function holds
  (f1 - f2)(#)f3 = f1(#)f3 - f2(#)f3
proof
  let f1,f2,f3 be complex-valued Function;
  (-f2)(#)f3 = -(f2(#)f3) by Th17;
  hence thesis by Th15;
end;

theorem
  for f1,f2,f3 being complex-valued Function holds
  f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) by Th19;

theorem T111:
  for f1,f2 being complex-valued Function holds
  r(#)(f1 + f2) = r(#)f1 + r(#)f2
proof
  let f1,f2 be complex-valued Function;
  thus
A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by VALUED_1:def 5
    .= dom f1 /\ dom f2 by VALUED_1:def 1
    .= dom f1 /\ dom (r(#)f2) by VALUED_1:def 5
    .= dom (r(#)f1) /\ dom (r(#)f2) by VALUED_1:def 5
    .= dom (r(#)f1 + r(#)f2) by VALUED_1:def 1;
    let c be object;
    assume
A2: c in dom (r(#)(f1 + f2));
    then
A3: c in dom (f1 + f2) by VALUED_1:def 5;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,VALUED_1:def 1;
    then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
    thus (r(#)(f1 + f2)).c = r * ((f1 + f2).c) by A2,VALUED_1:def 5
      .= r * (((f1.c)) + ((f2.c))) by A3,VALUED_1:def 1
      .= r * ((f1.c)) + r * ((f2.c))
      .= (r(#)f1).c + r * ((f2.c)) by A5,VALUED_1:def 5
      .= (r(#)f1).c + (r(#)f2).c by A6,VALUED_1:def 5
      .= (r(#)f1 + r(#)f2).c by A1,A2,VALUED_1:def 1;
end;

theorem
  for f being complex-valued Function holds (r*q)(#)f = r(#)(q(#)f)
proof
  let f be complex-valued Function;
  thus
A1: dom ((r*q) (#) f) = dom f by VALUED_1:def 5
    .= dom (q(#)f) by VALUED_1:def 5
    .= dom (r(#)(q(#)f)) by VALUED_1:def 5;
    let c be object;
    assume
A2: c in dom ((r*q)(#)f);
    then
A3: c in dom (q(#)f) by A1,VALUED_1:def 5;
    thus ((r*q)(#)f).c = r*q * (f.c) by A2,VALUED_1:def 5
    .= r*(q * (f.c))
    .= r * ((q(#)f).c) by A3,VALUED_1:def 5
    .= (r(#)(q(#)f)).c by A1,A2,VALUED_1:def 5;
  end;
  
T1: now
  let f be complex-valued Function;
  thus 1(#)f = f
  proof
    thus dom(1(#)f) = dom f by VALUED_1:def 5;
    let c be object;
    assume c in dom (1(#)f);
    hence (1(#)f).c = 1 * (f.c) by VALUED_1:def 5
    .= (f.c);
  end;
end;

T2:
 now
  let f be complex-valued Function;
  let r;
  thus r(#)(-f) = -(r(#)f)
  proof
    thus dom(r(#)(-f)) = dom(-f) by VALUED_1:def 5
    .= dom f by VALUED_1:8
    .= dom(r(#)f) by VALUED_1:def 5
    .= dom(-(r(#)f)) by VALUED_1:8;
    let c be object;
    assume c in dom (r(#)(-f));
    thus (r(#)(-f)).c = r * ((-f).c) by VALUED_1:6
    .= r * -(f.c) by VALUED_1:8
    .= -r*(f.c)
    .= -(r(#)f).c by VALUED_1:6
    .= (-(r(#)f)).c by VALUED_1:8;
  end;
end;

theorem
  for f1,f2 being complex-valued Function holds
  r(#)(f1 - f2) = r(#)f1 - r(#)f2
proof
  let f1,f2 be complex-valued Function;
  r(#)(-f2) = -r(#)f2 by T2;
  hence thesis by T111;
end;

theorem
  for f1,f2 being complex-valued Function holds f1-f2 = (-1)(#)(f2-f1)
proof
  let f1,f2 be complex-valued Function;
  thus
A1: dom (f1 - f2) = dom f2 /\ dom f1 by VALUED_1:12
    .= dom (f2 - f1) by VALUED_1:12
    .= dom ((-1)(#)(f2 - f1)) by VALUED_1:def 5;
A2: dom (f1 - f2) = dom f2 /\ dom f1 by VALUED_1:12
      .= dom (f2 - f1) by VALUED_1:12;
    let c be object such that
A3: c in dom (f1-f2);
    thus (f1 - f2).c = ((f1.c)) - ((f2.c)) by A3,VALUED_1:13
      .= (-1)*(((f2.c)) - ((f1.c)))
      .= (-1)*((f2 - f1).c) by A3,A2,VALUED_1:13
      .= ((-1)(#)(f2 - f1)).c by A1,A3,VALUED_1:def 5;
end;

theorem Tmp:
  for f1,f2,f3 being complex-valued Function holds
  f1 - (f2 + f3) = f1 - f2 - f3
proof
  let f1,f2,f3 be complex-valued Function;
  thus
A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by VALUED_1:12
    .= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:def 1
    .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
    .= dom (f1 - f2) /\ dom f3 by VALUED_1:12
    .= dom (f1 - f2 - f3) by VALUED_1:12;
    let c be object;
    assume
A2: c in dom (f1 - (f2 + f3));
    then c in dom f1 /\ dom (f2 + f3) by VALUED_1:12;
    then
A3: c in dom (f2 + f3) by XBOOLE_0:def 4;
    c in dom (f1 - f2) /\ dom f3 by A1,A2,VALUED_1:12;
    then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
    thus (f1 - (f2 + f3)).c = ((f1.c)) - (f2 + f3).c by A2,VALUED_1:13
    .= ((f1.c)) - (((f2.c)) + (f3.c)) by A3,VALUED_1:def 1
      .= ((f1.c)) - ((f2.c)) - (f3.c)
      .= (f1 - f2).c - (f3.c) by A4,VALUED_1:13
      .= (f1 - f2 - f3).c by A1,A2,VALUED_1:13;
end;

theorem
  for f being complex-valued Function holds 1(#)f = f by T1;

theorem
  for f1,f2,f3 being complex-valued Function holds
  f1 - (f2 - f3) = f1 - f2 + f3
proof
  let f1,f2,f3 be complex-valued Function;
  thus f1 - (f2 - f3) = f1 - f2 - (-f3) by Tmp
  .= f1 - f2 + f3;
end;

theorem
  for f1,f2,f3 being complex-valued Function holds
  f1 + (f2 - f3) = f1 + f2 - f3 by Tassoc;

theorem Th29:
  for f1,f2 being complex-valued Function holds
  |.f1(#)f2.| = |.f1.|(#)|.f2.|
proof
  let f1,f2 be complex-valued Function;
  thus dom (|.f1 (#) f2.|) = dom (f1 (#) f2) by VALUED_1:def 11
    .= dom f1 /\ dom f2 by VALUED_1:def 4
    .= dom f1 /\ dom (|.f2.|) by VALUED_1:def 11
    .= dom (|.f1.|) /\ dom (|.f2.|) by VALUED_1:def 11
    .= dom (|.f1.|(#)|.f2.|) by VALUED_1:def 4;
    let c be object;
    assume c in dom (|.f1 (#) f2.|);
    then
A5: c in dom (f1 (#) f2) by VALUED_1:def 11;
    thus (|.(f1(#)f2).|).c = |.(f1(#)f2).c.| by VALUED_1:18
      .= |.((f1.c)) * ((f2.c)).| by A5,VALUED_1:def 4
      .= |.((f1.c)).| * |.((f2.c)).| by COMPLEX1:65
      .= ((|.f1.|).c) *( |.((f2.c)).|) by VALUED_1:18
      .= ((|.f1.|).c) * ((|.f2.|).c) by VALUED_1:18
      .= (|.f1.|(#)|.f2.|).c by VALUED_1:5;
end;

theorem Th30:
  for f being complex-valued Function holds |.r(#)f.| = |.r.|(#)|.f.|
proof
  let f be complex-valued Function;
A1: dom f = dom (|.f.|) by VALUED_1:def 11;
    thus
A2: dom (|.r(#)f.|) = dom (r(#)f) by VALUED_1:def 11
    .= dom f by VALUED_1:def 5
    .= dom (|.r.|(#)|.f.|) by A1,VALUED_1:def 5;
    let c be object;
    assume
A3: c in dom (|.r(#)f.|);
    then
A4: c in dom (r(#)f) by VALUED_1:def 11;
    thus (|.r(#)f.|).c = |.(r(#)f).c.| by VALUED_1:18
      .=|.r*((f.c)).| by A4,VALUED_1:def 5
      .=|.r.|*|.((f.c)).| by COMPLEX1:65
      .=|.r.|*((|.f.|).c) by VALUED_1:18
      .=(|.r.|(#)|.f.|).c by A2,A3,VALUED_1:def 5;
end;

theorem
  for f being complex-valued Function holds -f = (-1)(#)f;

theorem
  for f1,f2 being complex-valued Function holds (-f1)(#)f2 = -(f1(#)f2)
  by Th17;

theorem
  for f1,f2 being complex-valued Function holds f1 - (-f2) = f1 + f2;

theorem Th33:
  f^^ = f|(dom (f^))
proof
A1: dom (f^^) = dom (f|(dom (f^))) by Th11;
  now
    let c;
    assume
A2: c in dom (f^^);
    then c in dom f /\ dom (f^) by A1,RELAT_1:61;
    then
A3: c in dom (f^) by XBOOLE_0:def 4;
    thus (f^^)/.c = ((f^)/.c)" by A2,Def2
      .= (((f/.c))")" by A3,Def2
      .= (f|(dom (f^)))/.c by A1,A2,PARTFUN2:15;
  end;
  hence thesis by A1,PARTFUN2:1;
end;

theorem Th34:
  (f1(#)f2)^ = (f1^)(#)(f2^)
proof
A1: dom ((f1(#)f2)^) = dom (f1(#)f2) \ (f1(#)f2)"{0c} by Def2
    .= (dom f1 \ f1"{0c}) /\ (dom f2 \ (f2)"{0c}) by Th7
    .= dom (f1^) /\ (dom f2 \ (f2)"{0c}) by Def2
    .= dom (f1^) /\ dom (f2^) by Def2
    .= dom ((f1^) (#) (f2^)) by Th3;
  now
    let c;
    assume
A2: c in dom ((f1(#)f2)^);
    then c in dom (f1(#)f2) \ (f1(#)f2)"{0c} by Def2;
    then
A3: c in dom (f1(#)f2) by XBOOLE_0:def 5;
A4: c in dom (f1^) /\ dom (f2^) by A1,A2,Th3;
    then
A5: c in dom (f1^) by XBOOLE_0:def 4;
A6: c in dom (f2^) by A4,XBOOLE_0:def 4;
    thus ((f1(#)f2)^)/.c = ((f1(#)f2)/.c)" by A2,Def2
      .= (((f1/.c)) * ((f2/.c)))" by A3,Th3
      .= (((f1/.c)))"* (((f2/.c)))" by XCMPLX_1:204
      .= ((f1^)/.c)*(((f2/.c)))" by A5,Def2
      .= ((f1^)/.c) *((f2^)/.c) by A6,Def2
      .= ((f1^) (#) (f2^))/.c by A1,A2,Th3;
  end;
  hence thesis by A1,PARTFUN2:1;
end;

theorem Th35:
  r <> 0 implies (r(#)f)^ = r" (#) (f^)
proof
  assume
A1: r<>0;
A2: dom ((r(#)f)^) = dom (r(#)f) \ (r(#)f)"{0c} by Def2
    .= dom (r(#)f) \ f"{0c} by A1,Th12
    .= dom f \ f"{0c} by Th4
    .= dom (f^) by Def2
    .= dom (r"(#)(f^)) by Th4;
  now
    let c;
    assume
A3: c in dom ((r(#)f)^);
    then
A4: c in dom (f^) by A2,Th4;
    c in dom (r(#)f) \ (r(#)f)"{0c} by A3,Def2;
    then
A5: c in dom (r(#)f) by XBOOLE_0:def 5;
    thus ((r(#)f)^)/.c = ((r(#)f)/.c)" by A3,Def2
      .= (r*((f/.c)))" by A5,Th4
      .= r"* ((f/.c))" by XCMPLX_1:204
      .= r"* ((f^)/.c) by A4,Def2
      .= (r" (#) (f^))/.c by A2,A3,Th4;
  end;
  hence thesis by A2,PARTFUN2:1;
end;

Lm2: (-1r)"=-1r by COMPLEX1:def 4;

theorem
  (-f)^ = (-1r)(#)(f^) by Lm2,Th35,COMPLEX1:def 4;

theorem Th37:
  |.f.|^ = |. f^ .|
proof
A1: dom ((|.f.|)^) = dom (|.f.|) \ (|.f.|)"{0} by RFUNCT_1:def 2
    .= dom f \ (|.f.|)"{0} by VALUED_1:def 11
    .= dom f \ f"{0c} by Th10
    .= dom (f^) by Def2
    .= dom (|.(f^).|) by VALUED_1:def 11;
  now
    let c;
A2: dom f = dom |.f.| by VALUED_1:def 11;
    assume
A3: c in dom ((|.f.|)^);
    then
A4: c in dom (f^) by A1,VALUED_1:def 11;
    c in dom (|.f.|) \ (|.f.|)"{0} by A3,RFUNCT_1:def 2;
    then
A5: c in dom (|.f.|) by XBOOLE_0:def 5;
    thus ((|.f.|)^).c = ((|.f.|).c)" by A3,RFUNCT_1:def 2
      .= (|.(f.c) .|)" by VALUED_1:18
      .= (|.(f/.c) .|)" by A5,A2,PARTFUN1:def 6
      .= |.1r.|/|.(f/.c) .| by COMPLEX1:48,XCMPLX_1:215
      .= |.1r/(f/.c) .| by COMPLEX1:67
      .= |.((f/.c))" .| by COMPLEX1:def 4,XCMPLX_1:215
      .= |.(f^)/.c .| by A4,Def2
      .= |.(f^).c .| by A4,PARTFUN1:def 6
      .= (|.(f^).|).c by VALUED_1:18;
  end;
  hence thesis by A1,PARTFUN1:5;
end;

theorem Th38:
  f/g = f (#) (g^)
proof
A1: now
    let c;
    assume
A2: c in dom (f/g);
    then c in dom f /\ (dom g \ g"{0c}) by Def1;
    then
A3: c in dom f /\ dom (g^) by Def2;
    then
A4: c in dom (g^) by XBOOLE_0:def 4;
A5: c in dom (f (#) (g^)) by A3,Th3;
    thus (f/g)/.c = (f/.c) * (g/.c)" by A2,Def1
      .= (f/.c) * ((g^)/.c) by A4,Def2
      .= (f (#) (g^))/.c by A5,Th3;
  end;
  dom (f/g) = dom f /\ (dom g \ g"{0c}) by Def1
    .= dom f /\ dom (g^) by Def2
    .= dom (f(#)(g^)) by Th3;
  hence thesis by A1,PARTFUN2:1;
end;

theorem Th39:
  r(#)(g/f) = (r(#)g)/f
proof
  thus r(#)(g/f) = r(#)(g(#)(f^)) by Th38
    .= (r(#)g)(#)(f^) by Th17
    .= (r(#)g)/f by Th38;
end;

theorem
  (f/g)(#)g = (f|dom(g^))
proof
A1: dom ((f/g)(#)g) = dom (f/g) /\ dom g by Th3
    .= dom f /\ (dom g \ g"{0c}) /\ dom g by Def1
    .= dom f /\ ((dom g \ g"{0c}) /\ dom g) by XBOOLE_1:16
    .= dom f /\ (dom (g^) /\ dom g) by Def2
    .= dom f /\ dom (g^) by Th6,XBOOLE_1:28
    .= dom (f|(dom (g^))) by RELAT_1:61;
  now
    let c;
    assume
A2: c in dom ((f/g)(#)g);
    then
A3: c in dom f /\ dom (g^) by A1,RELAT_1:61;
    then
A4: c in dom (f(#)(g^)) by Th3;
A5: c in dom (g^) by A3,XBOOLE_0:def 4;
    then
A6: g/.c <> 0c by Th8;
    thus ((f/g)(#)g)/.c = ((f/g)/.c) * (g/.c )by A2,Th3
      .= (f(#)(g^))/.c * (g/.c) by Th38
      .= ((f/.c)) *((g^)/.c) * (g/.c) by A4,Th3
      .= ((f/.c))*(g/.c)"*(g/.c) by A5,Def2
      .= ((f/.c))*((g/.c)" * (g/.c))
      .= ((f/.c))*1r by A6,COMPLEX1:def 4,XCMPLX_0:def 7
      .= (f|(dom (g^)))/.c by A1,A2,COMPLEX1:def 4,PARTFUN2:15;
  end;
  hence thesis by A1,PARTFUN2:1;
end;

theorem Th41:
  (f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1)
proof
A1: now
    let c;
    assume
A2: c in dom ((f/g)(#)(f1/g1));
    then c in dom (f/g) /\ dom (f1/g1) by Th3;
    then
A3: c in dom (f (#)(g^)) /\ dom (f1/g1) by Th38;
    then
A4: c in dom (f (#)(g^)) by XBOOLE_0:def 4;
    then
A5: c in dom f /\ dom(g^) by Th3;
    c in dom (f (#)(g^)) /\ dom (f1(#)(g1^)) by A3,Th38;
    then
A6: c in dom (f1(#)(g1^)) by XBOOLE_0:def 4;
    then
A7: c in dom f1 /\ dom(g1^) by Th3;
    then
A8: c in dom f1 by XBOOLE_0:def 4;
    c in dom f by A5,XBOOLE_0:def 4;
    then c in dom f /\ dom f1 by A8,XBOOLE_0:def 4;
    then
A9: c in dom (f(#)f1) by Th3;
A10: c in dom(g1^) by A7,XBOOLE_0:def 4;
    c in dom(g^) by A5,XBOOLE_0:def 4;
    then c in dom (g^) /\ dom (g1^) by A10,XBOOLE_0:def 4;
    then
A11: c in dom((g^)(#)(g1^)) by Th3;
    then c in dom((g(#)g1)^) by Th34;
    then c in dom (f(#)f1) /\ dom((g(#)g1)^) by A9,XBOOLE_0:def 4;
    then
A12: c in dom ((f(#)f1)(#)((g(#)g1)^)) by Th3;
    thus ((f/g)(#)(f1/g1))/.c = ((f/g)/.c)* ((f1/g1)/.c) by A2,Th3
      .= ((f(#)(g^))/.c) * ((f1/g1)/.c) by Th38
      .= ((f(#)(g^))/.c) * ((f1(#)(g1^))/.c) by Th38
      .= ((f/.c)) * ((g^)/.c) *((f1(#)(g1^))/.c) by A4,Th3
      .= ((f/.c)) * ((g^)/.c) * ((((f1/.c)))* ((g1^)/.c)) by A6,Th3
      .= ((f/.c)) * ((((f1/.c))) * (((g^)/.c) * ((g1^)/.c)))
      .= ((f/.c)) * ((((f1/.c))) * (((g^)(#)(g1^))/.c)) by A11,Th3
      .= ((f/.c)) * (((f1/.c))) * (((g^)(#)(g1^))/.c)
      .= ((f/.c)) * (((f1/.c))) * (((g(#)g1)^)/.c) by Th34
      .= ((f(#)f1)/.c) * (((g(#)g1)^)/.c) by A9,Th3
      .= ((f(#)f1)(#)((g(#)g1)^))/.c by A12,Th3
      .= ((f(#)f1)/(g(#)g1))/.c by Th38;
  end;
  dom ((f/g)(#)(f1/g1)) = dom (f/g) /\ dom (f1/g1) by Th3
    .= dom f /\ (dom g \ g"{0c}) /\ dom (f1/g1) by Def1
    .= dom f /\ (dom g \ g"{0c}) /\ (dom f1 /\ (dom g1 \ g1"{0c})) by Def1
    .= dom f /\ ((dom g \ g"{0c}) /\ (dom f1 /\ (dom g1 \ g1"{0c}))) by
XBOOLE_1:16
    .= dom f /\ (dom f1 /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c}))) by
XBOOLE_1:16
    .= dom f /\ dom f1 /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c})) by
XBOOLE_1:16
    .= dom (f(#)f1) /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c})) by Th3
    .= dom (f(#)f1) /\ (dom (g(#)g1) \ (g(#)g1)"{0c}) by Th7
    .= dom ((f(#)f1)/(g(#)g1)) by Def1;
  hence thesis by A1,PARTFUN2:1;
end;

theorem Th42:
  (f1/f2)^ = (f2|dom(f2^))/f1
proof
  thus (f1/f2)^ = (f1(#)(f2^))^ by Th38
    .= (f1^)(#)(f2^^) by Th34
    .= (f2|dom(f2^))(#)(f1^) by Th33
    .= (f2|dom(f2^))/f1 by Th38;
end;

theorem Th43:
  g (#) (f1/f2) = (g (#) f1)/f2
proof
  thus g (#) (f1/f2) = g (#) (f1 (#) (f2^)) by Th38
    .= g (#) f1 (#) (f2^) by Th14
    .= (g (#) f1)/f2 by Th38;
end;

theorem
  g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1
proof
  thus g/(f1/f2) = g (#) ((f1/f2)^) by Th38
    .= g (#) ((f2|dom(f2^))/f1) by Th42
    .= (g (#) (f2|dom(f2^)))/f1 by Th43;
end;

theorem
  -f/g = (-f)/g & f/(-g) = -f/g
proof
  thus -f/g = (-f)/g by Th39;
  thus f/(-g) = f (#) ((-g)^) by Th38
    .= f (#) ((-1r) (#) (g^)) by Lm2,Th35,COMPLEX1:def 4
    .= -(f (#) (g^)) by Th18,COMPLEX1:def 4
    .= -(f/g) by Th38;
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 Th38
    .= f1(#)(f^) + f2(#)(f^) by Th38
    .= (f1+f2) (#) (f^) by Th15
    .= (f1+f2)/f by Th38;
  thus f1/f - f2/f = f1(#)(f^) - f2/f by Th38
    .= f1(#)(f^) -f2(#)(f^) by Th38
    .= (f1-f2)(#)(f^) by Th19
    .= (f1-f2)/f by Th38;
end;

theorem Th47:
  f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g)
proof
A1: now
    let c;
A2: dom (f^) c= dom f by Th6;
    assume
A3: c in dom ((f1/f) + (g1/g));
    then
A4: c in dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1;
    then
A5: c in dom (f1/f) by XBOOLE_0:def 4;
A6: c in dom (g1/g) by A4,XBOOLE_0:def 4;
A7: c in dom (f1 (#)(f^)) /\ dom (g1/g) by A4,Th38;
    then c in dom (f1 (#)(f^)) by XBOOLE_0:def 4;
    then
A8: c in dom f1 /\ dom(f^) by Th3;
    then
A9: c in dom(f^) by XBOOLE_0:def 4;
    then
A10: (f/.c) <> 0c by Th8;
    c in dom (f1 (#)(f^)) /\ dom (g1(#)(g^)) by A7,Th38;
    then c in dom (g1(#)(g^)) by XBOOLE_0:def 4;
    then
A11: c in dom g1 /\ dom(g^) by Th3;
    then
A12: c in dom(g^) by XBOOLE_0:def 4;
    then
A13: g/.c <> 0c by Th8;
    c in dom g1 by A11,XBOOLE_0:def 4;
    then c in dom g1 /\ dom f by A9,A2,XBOOLE_0:def 4;
    then
A14: c in dom (g1(#)f) by Th3;
A15: dom (g^) c= dom g by Th6;
    then c in dom f /\ dom g by A9,A12,A2,XBOOLE_0:def 4;
    then
A16: c in dom (f(#)g) by Th3;
    c in dom f1 by A8,XBOOLE_0:def 4;
    then c in dom f1 /\ dom g by A12,A15,XBOOLE_0:def 4;
    then
A17: c in dom (f1(#)g) by Th3;
    then c in dom (f1(#)g) /\ dom (g1(#)f) by A14,XBOOLE_0:def 4;
    then
A18: c in dom (f1(#)g + g1(#)f) by VALUED_1:def 1;
    c in dom (f^) /\ dom (g^) by A9,A12,XBOOLE_0:def 4;
    then c in dom ((f^)(#)(g^)) by Th3;
    then c in dom ((f(#)g)^) by Th34;
    then c in dom (f1(#)g + g1(#)f) /\ dom ((f(#)g)^) by A18,XBOOLE_0:def 4;
    then c in dom ((f1(#)g + g1(#)f)(#)((f(#)g)^)) by Th3;
    then
A19: c in dom ((f1(#)g + g1(#)f)/(f(#)g)) by Th38;
    thus (f1/f + g1/g)/.c = (f1/f)/.c + (g1/g)/.c by A3,Th1
      .= (((f1/.c))) * ((f/.c))" + (g1/g)/.c by A5,Def1
      .= (((f1/.c))) *(1r*((f/.c))") + (g1/.c) * 1r * (g/.c)" by A6,Def1,
COMPLEX1:def 4
      .= (((f1/.c))) *((g/.c) *(g/.c)"* ((f/.c))") + (g1/.c) * (1r * (g/.c)"
    ) by A13,COMPLEX1:def 4,XCMPLX_0:def 7
      .= (((f1/.c))) *(g/.c *((g/.c)"* ((f/.c))")) + (g1/.c) * (((f/.c)) *((
    f/.c))" * (g/.c)") by A10,COMPLEX1:def 4,XCMPLX_0:def 7
      .= (((f1/.c))) *((g/.c) *((g/.c * (f/.c))")) + (g1/.c) * (((f/.c)) *((
    (f/.c))" * (g/.c)")) by XCMPLX_1:204
      .= (((f1/.c))) *((g/.c) *(((f/.c)* (g/.c))")) + (g1/.c) * (((f/.c)) *(
    ((f/.c) * (g/.c))")) by XCMPLX_1:204
      .= (((f1/.c))) *((g/.c) * ((f(#)g)/.c)") + (g1/.c) * (((f/.c)) *(((f/.
    c) * (g/.c))")) by A16,Th3
      .= (((f1/.c))) *(g/.c) * ((f(#)g)/.c)" + (g1/.c) * (((f/.c)) * ((f(#)
    g)/.c)") by A16,Th3
      .= (f1(#)g)/.c * ((f(#)g)/.c)" + (g1/.c) *(f/.c) *((f(#)g)/.c)" by A17
,Th3
      .= (f1(#)g)/.c * ((f(#)g)/.c)" + (g1(#)f)/.c *((f(#)g)/.c)" by A14,Th3
      .= ((f1(#)g)/.c + (g1(#)f)/.c) *((f(#)g)/.c)"
      .= (f1(#)g + g1(#)f)/.c *((f(#)g)/.c)" by A18,Th1
      .= ((f1(#)g + g1(#)f)/(f(#)g))/.c by A19,Def1;
  end;
  dom ((f1/f) + (g1/g)) = dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1
    .= dom f1 /\ (dom f \ f"{0c}) /\ dom (g1/g) by Def1
    .= dom f1 /\ (dom f \ f"{0c}) /\ (dom g1 /\ (dom g \ g"{0c})) by Def1
    .= dom f1 /\ (dom f /\ (dom f \ f"{0c})) /\ (dom g1 /\ (dom g \ g"{0c}))
  by Th6
    .= dom f /\ (dom f \ f"{0c}) /\ dom f1 /\ (dom g /\ (dom g \ g"{0c}) /\
  dom g1) by Th6
    .= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0c}) /\
  dom g1)) by XBOOLE_1:16
    .= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0c}))
  /\ dom g1) by XBOOLE_1:16
    .= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ dom g /\ (dom g \ g"{0c}) /\
  dom g1) by XBOOLE_1:16
    .= dom f /\ (dom f \ f"{0c}) /\ (dom (f1(#) g) /\ (dom g \ g"{0c}) /\
  dom g1) by Th3
    .= dom f /\ (dom f \ f"{0c}) /\ (dom (f1(#)g) /\ (dom g1 /\ (dom g \ g"{
  0c}))) by XBOOLE_1:16
    .= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ dom f /\ (dom g1 /\ (dom g \ g"{
  0c}))) by XBOOLE_1:16
    .= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom f /\ (dom g1 /\ (dom g \ g"
  {0c})))) by XBOOLE_1:16
    .= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom g1 /\ dom f /\ (dom g \ g"{
  0c}))) by XBOOLE_1:16
    .= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom (g1(#)f) /\ (dom g \ g"{0c}
  ))) by Th3
    .= dom (f1(#)g) /\ (dom (g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c}
  ))) by XBOOLE_1:16
    .= dom (f1(#)g) /\ dom (g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c})
  ) by XBOOLE_1:16
    .= dom (f1(#)g + g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c})) by
VALUED_1:def 1
    .= dom (f1(#)g + g1(#)f) /\ (dom (f(#)g) \ (f(#)g)"{0c}) by Th7
    .= dom ((f1(#)g + g1(#)f)/(f(#)g)) by Def1;
  hence thesis by A1,PARTFUN2:1;
end;

theorem
  (f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1)
proof
  thus (f/g)/(f1/g1) = (f/g)(#)((f1/g1)^) by Th38
    .= (f/g)(#)(((g1|dom(g1^)))/f1) by Th42
    .= (f(#)(g1|dom(g1^)))/(g(#)f1) by Th41;
end;

theorem
  f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g)
proof
  thus f1/f - g1/g = f1/f + ((-1r)(#) g1)/g by Th39,COMPLEX1:def 4
    .= (f1(#)g + (-1r)(#) g1(#)f)/(f(#)g) by Th47
    .= (f1(#)g - (g1(#)f))/(f(#)g) by Th17,COMPLEX1:def 4;
end;

theorem
  |.f1/f2.| = |.f1.|/|.f2.|
proof
  thus |.f1/f2.| = |.f1(#)(f2^).| by Th38
    .= |.f1.|(#)|.(f2^).| by Th29
    .= |.f1.|(#)((|.f2.|)^) by Th37
    .= |.f1.|/|.f2.| by RFUNCT_1:31;
end;

theorem Th51:
  (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: now
    let c;
    assume
A2: c in dom ((f1+f2)|X);
    then
A3: c in dom (f1+f2) /\ X by RELAT_1:61;
    then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1+f2) by A3,XBOOLE_0:def 4;
    then
A6: c in dom f1 /\ dom f2 by VALUED_1:def 1;
    then c in dom f2 by XBOOLE_0:def 4;
    then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
    then
A7: c in dom (f2|X) by RELAT_1:61;
    c in dom f1 by A6,XBOOLE_0:def 4;
    then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
    then
A8: c in dom (f1|X) by RELAT_1:61;
    then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
    then
A9: c in dom ((f1|X) + (f2|X)) by VALUED_1:def 1;
    thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:15
      .= (((f1/.c))) + (((f2/.c))) by A5,Th1
      .= ((f1|X)/.c) + (((f2/.c))) by A8,PARTFUN2:15
      .= ((f1|X)/.c) + ((f2|X)/.c) by A7,PARTFUN2:15
      .= ((f1|X)+(f2|X))/.c by A9,Th1;
  end;
  dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ (X /\ X) by VALUED_1:def 1
    .= 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:61
    .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
    .= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
    .= dom ((f1|X)+(f2|X)) by VALUED_1:def 1;
  hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:1;
A10: now
    let c;
    assume
A11: c in dom ((f1+f2)|X);
    then
A12: c in dom (f1+f2) /\ X by RELAT_1:61;
    then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1+f2) by A12,XBOOLE_0:def 4;
    then
A15: c in dom f1 /\ dom f2 by VALUED_1:def 1;
    then c in dom f1 by XBOOLE_0:def 4;
    then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
    then
A16: c in dom (f1|X) by RELAT_1:61;
    c in dom f2 by A15,XBOOLE_0:def 4;
    then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
    then
A17: c in dom ((f1|X) + f2) by VALUED_1:def 1;
    thus ((f1+f2)|X)/.c = (f1+f2)/.c by A11,PARTFUN2:15
      .= (((f1/.c))) +(((f2/.c))) by A14,Th1
      .= ((f1|X)/.c) +(((f2/.c))) by A16,PARTFUN2:15
      .= ((f1|X)+f2)/.c by A17,Th1;
  end;
  dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ X by VALUED_1:def 1
    .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
    .= dom (f1|X) /\ dom f2 by RELAT_1:61
    .= dom ((f1|X)+ f2) by VALUED_1:def 1;
  hence (f1+f2)|X = f1|X + f2 by A10,PARTFUN2:1;
A18: now
    let c;
    assume
A19: c in dom ((f1+f2)|X);
    then
A20: c in dom (f1+f2) /\ X by RELAT_1:61;
    then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1+f2) by A20,XBOOLE_0:def 4;
    then
A23: c in dom f1 /\ dom f2 by VALUED_1:def 1;
    then c in dom f2 by XBOOLE_0:def 4;
    then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
    then
A24: c in dom (f2|X) by RELAT_1:61;
    c in dom f1 by A23,XBOOLE_0:def 4;
    then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
    then
A25: c in dom (f1 + (f2|X)) by VALUED_1:def 1;
    thus ((f1+f2)|X)/.c = (f1+f2)/.c by A19,PARTFUN2:15
      .= (((f1/.c))) +(((f2/.c))) by A22,Th1
      .= (((f1/.c))) +((f2|X)/.c) by A24,PARTFUN2:15
      .= (f1+(f2|X))/.c by A25,Th1;
  end;
  dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ X by VALUED_1:def 1
    .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
    .= dom f1 /\ dom (f2|X) by RELAT_1:61
    .= dom (f1 + (f2|X)) by VALUED_1:def 1;
  hence thesis by A18,PARTFUN2:1;
end;

theorem Th52:
  (f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)
  f2)|X = f1 (#) f2|X
proof
A1: now
    let c;
    assume
A2: c in dom ((f1(#)f2)|X);
    then
A3: c in dom (f1(#)f2) /\ X by RELAT_1:61;
    then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1(#)f2) by A3,XBOOLE_0:def 4;
    then
A6: c in dom f1 /\ dom f2 by Th3;
    then c in dom f2 by XBOOLE_0:def 4;
    then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
    then
A7: c in dom (f2|X) by RELAT_1:61;
    c in dom f1 by A6,XBOOLE_0:def 4;
    then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
    then
A8: c in dom (f1|X) by RELAT_1:61;
    then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
    then
A9: c in dom ((f1|X) (#) (f2|X)) by Th3;
    thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:15
      .= (((f1/.c))) *(((f2/.c))) by A5,Th3
      .= ((f1|X)/.c) *(((f2/.c))) by A8,PARTFUN2:15
      .= ((f1|X)/.c) *((f2|X)/.c) by A7,PARTFUN2:15
      .= ((f1|X)(#)(f2|X))/.c by A9,Th3;
  end;
  dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ (X /\ X) by Th3
    .= 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:61
    .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
    .= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
    .= dom ((f1|X)(#)(f2|X)) by Th3;
  hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN2:1;
A10: now
    let c;
    assume
A11: c in dom ((f1(#)f2)|X);
    then
A12: c in dom (f1(#)f2) /\ X by RELAT_1:61;
    then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1(#)f2) by A12,XBOOLE_0:def 4;
    then
A15: c in dom f1 /\ dom f2 by Th3;
    then c in dom f1 by XBOOLE_0:def 4;
    then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
    then
A16: c in dom (f1|X) by RELAT_1:61;
    c in dom f2 by A15,XBOOLE_0:def 4;
    then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
    then
A17: c in dom ((f1|X) (#) f2) by Th3;
    thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A11,PARTFUN2:15
      .= (((f1/.c))) *(((f2/.c))) by A14,Th3
      .= ((f1|X)/.c) *(((f2/.c))) by A16,PARTFUN2:15
      .= ((f1|X)(#)f2)/.c by A17,Th3;
  end;
  dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ X by Th3
    .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
    .= dom (f1|X) /\ dom f2 by RELAT_1:61
    .= dom ((f1|X)(#) f2) by Th3;
  hence (f1(#)f2)|X = f1|X (#) f2 by A10,PARTFUN2:1;
A18: now
    let c;
    assume
A19: c in dom ((f1(#)f2)|X);
    then
A20: c in dom (f1(#)f2) /\ X by RELAT_1:61;
    then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1(#)f2) by A20,XBOOLE_0:def 4;
    then
A23: c in dom f1 /\ dom f2 by Th3;
    then c in dom f2 by XBOOLE_0:def 4;
    then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
    then
A24: c in dom (f2|X) by RELAT_1:61;
    c in dom f1 by A23,XBOOLE_0:def 4;
    then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
    then
A25: c in dom (f1 (#) (f2|X)) by Th3;
    thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A19,PARTFUN2:15
      .= (((f1/.c))) *(((f2/.c))) by A22,Th3
      .= (((f1/.c))) *((f2|X)/.c) by A24,PARTFUN2:15
      .= (f1(#)(f2|X))/.c by A25,Th3;
  end;
  dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
    .= dom f1 /\ dom f2 /\ X by Th3
    .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
    .= dom f1 /\ dom (f2|X) by RELAT_1:61
    .= dom (f1 (#) (f2|X)) by Th3;
  hence thesis by A18,PARTFUN2:1;
end;

theorem Th53:
  (-f)|X = -(f|X) & (f^)|X = (f|X)^ & (|.f.|)|X = |.(f|X).|
proof
A1: dom ((f^)|X) = dom (f^) /\ X by RELAT_1:61
    .= (dom f \ f"{0c}) /\ X by Def2
    .= dom f /\ X \ f"{0c} /\ X by XBOOLE_1:50
    .= dom (f|X) \ X /\ f"{0c} by RELAT_1:61
    .= dom (f|X) \ (f|X)"{0c} by FUNCT_1:70
    .= dom ((f|X)^) by Def2;
A2: now
    let c;
    assume
A3: c in dom ((-f)|X);
    then
A4: c in dom (-f) /\ X by RELAT_1:61;
    then
A5: c in X by XBOOLE_0:def 4;
A6: c in dom (-f) by A4,XBOOLE_0:def 4;
    then c in dom f by Th5;
    then c in dom f /\ X by A5,XBOOLE_0:def 4;
    then
A7: c in dom (f|X) by RELAT_1:61;
    then
A8: c in dom (-(f|X)) by Th5;
    thus ((-f)|X)/.c = (-f)/.c by A3,PARTFUN2:15
      .= -((f/.c)) by A6,Th5
      .= -((f|X)/.c) by A7,PARTFUN2:15
      .= (-(f|X))/.c by A8,Th5;
  end;
  dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61
    .= dom f /\ X by Th5
    .= dom (f|X) by RELAT_1:61
    .= dom (-(f|X)) by Th5;
  hence (-f)|X = -(f|X) by A2,PARTFUN2:1;
A9: dom ((f|X)^) c= dom (f|X) by Th6;
  now
    let c;
    assume
A10: c in dom ((f^)|X);
    then c in dom (f^) /\ X by RELAT_1:61;
    then
A11: c in dom (f^) by XBOOLE_0:def 4;
    thus ((f^)|X)/.c = (f^)/.c by A10,PARTFUN2:15
      .= ((f/.c))" by A11,Def2
      .= ((f|X)/.c)" by A9,A1,A10,PARTFUN2:15
      .= ((f|X)^)/.c by A1,A10,Def2;
  end;
  hence (f^)|X = (f|X)^ by A1,PARTFUN2:1;
A12: dom ((|.f.|)|X) = dom (|.f.|) /\ X by RELAT_1:61
    .= dom f /\ X by VALUED_1:def 11
    .= dom (f|X) by RELAT_1:61
    .= dom (|.(f|X).|) by VALUED_1:def 11;
  now
    let c;
A13: dom |.f.| = dom f by VALUED_1:def 11;
    assume
A14: c in dom ((|.f.|)|X);
    then
A15: c in dom (f|X) by A12,VALUED_1:def 11;
    c in dom (|.f.|) /\ X by A14,RELAT_1:61;
    then
A16: c in dom (|.f.|) by XBOOLE_0:def 4;
    thus ((|.f.|)|X).c = (|.f.|).c by A14,FUNCT_1:47
      .= |.(f.c).| by VALUED_1:18
      .= |.(f/.c).| by A16,A13,PARTFUN1:def 6
      .= |.(f|X)/.c.| by A15,PARTFUN2:15
      .= |.(f|X).c.| by A15,PARTFUN1:def 6
      .= (|.(f|X).|).c by VALUED_1:18;
  end;
  hence thesis by A12,PARTFUN1:5;
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|X)+ (-f2)|X by Th51
    .= (f1|X) - (f2|X) by Th53;
  thus (f1-f2)|X = (f1|X)+ -f2 by Th51
    .= (f1|X) - f2;
  thus (f1-f2)|X = f1+ (-f2)|X by Th51
    .= f1 - (f2|X) by Th53;
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 Th38
    .= (f1|X) (#) (f2^|X) by Th52
    .= (f1|X) (#) ((f2|X)^) by Th53
    .= (f1|X)/(f2|X) by Th38;
  thus (f1/f2)|X = (f1(#)(f2^))|X by Th38
    .= (f1|X) (#) (f2^) by Th52
    .= (f1|X)/f2 by Th38;
  thus (f1/f2)|X = (f1(#)(f2^))|X by Th38
    .= f1 (#) (f2^)|X by Th52
    .= f1 (#) ((f2|X)^) by Th53
    .= f1/(f2|X) by Th38;
end;

theorem
  (r(#)f)|X = r(#)(f|X)
proof
A1: now
    let c;
    assume
A2: c in dom ((r(#)f)|X);
    then
A3: c in dom (r(#)f) /\ X by RELAT_1:61;
    then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (r(#)f) by A3,XBOOLE_0:def 4;
    then c in dom f by Th4;
    then c in dom f /\ X by A4,XBOOLE_0:def 4;
    then
A6: c in dom (f|X) by RELAT_1:61;
    then
A7: c in dom (r(#)(f|X)) by Th4;
    thus ((r(#)f)|X)/.c = (r(#)f)/.c by A2,PARTFUN2:15
      .= r*((f/.c)) by A5,Th4
      .= r*((f|X)/.c) by A6,PARTFUN2:15
      .= (r(#)(f|X))/.c by A7,Th4;
  end;
  dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:61
    .= dom f /\ X by Th4
    .= dom (f|X) by RELAT_1:61
    .= dom (r(#)(f|X)) by Th4;
  hence thesis by A1,PARTFUN2:1;
end;

begin

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::

theorem Th57:
  (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;
      hence dom (f1+f2) = C /\ C by VALUED_1:def 1
        .= C;
    end;
    assume f1+f2 is total;
    then dom (f1+f2) = C;
    then dom f1 /\ dom f2 = C by VALUED_1:def 1;
    then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
    hence dom f1 = C & dom f2 = C;
  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;
      hence dom (f1-f2) = C /\ C by Th2
        .= C;
    end;
    assume f1-f2 is total;
    then dom (f1-f2) = C;
    then dom f1 /\ dom f2 = C by Th2;
    then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
    hence dom f1 = C & dom f2 = C;
  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;
    hence dom (f1(#)f2) = C /\ C by Th3
      .= C;
  end;
  assume f1(#)f2 is total;
  then dom (f1(#)f2) = C;
  then dom f1 /\ dom f2 = C by Th3;
  then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
  hence dom f1 = C & dom f2 = C;
end;

theorem Th58:
  f is total iff r(#)f is total by Th4;

theorem
  f is total iff -f is total by Th58;

theorem
  f is total iff |.f.| is total by VALUED_1:def 11;

theorem Th61:
  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;
    f"{0c} c= C;
    then f"{0c} c= dom f \ f"{0c} by A1,Def2;
    hence f"{0} = {} by XBOOLE_1:38;
    then C = dom f \ {} by A1,Def2;
    hence dom f = C;
  end;
  assume
A2: f"{0} = {} & f is total;
  thus dom (f^) = dom f \ f"{0c} by Def2
    .= C by A2;
end;

theorem Th62:
  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 that
A1: f1 is total and
A2: f2"{0} = {} & f2 is total;
    f2^ is total by A2,Th61;
    then f1(#)(f2^) is total by A1;
    hence thesis by Th38;
  end;
  assume f1/f2 is total;
  then
A3: f1(#)(f2^) is total by Th38;
  hence f1 is total by Th57;
  f2^ is total by A3,Th57;
  hence thesis by Th61;
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;
  then dom (f1+f2) = C;
  hence (f1+f2)/.c = ((f1/.c)) + ((f2/.c)) by Th1;
  f1-f2 is total by A1;
  then dom (f1-f2) = C;
  hence (f1-f2)/.c = ((f1/.c)) - ((f2/.c)) by Th2;
  f1(#)f2 is total by A1;
  then dom (f1(#)f2) = C;
  hence thesis by Th3;
end;

theorem
  f is total implies (r(#)f)/.c = r * ((f/.c))
proof
  assume f is total;
  then r(#)f is total;
  then dom (r(#)f) = C;
  hence thesis by Th4;
end;

theorem
  f is total implies (-f)/.c = - (f/.c) & (|.f.|).c = |. (f/.c) .|
proof
  assume
A1: f is total;
  then |.f.| is total;
  then
A2: dom |.f.| = dom f & dom (|.f.|) = C by VALUED_1:def 11;
  -f is total by A1;
  then dom (-f) = C;
  hence (-f)/.c = - (f/.c) by Th5;
  thus (|.f.|).c = |. (f.c) .| by VALUED_1:18
    .= |. (f/.c) .| by A2,PARTFUN1:def 6;
end;

theorem
  f^ is total implies (f^)/.c = ((f/.c))"
by Def2;

theorem
  f1 is total & f2^ is total implies (f1/f2)/.c = ((f1/.c)) *(((f2/.c))) "
proof
  assume that
A1: f1 is total and
A2: f2^ is total;
  f2"{0c} = {} & f2 is total by A2,Th61;
  then f1/f2 is total by A1,Th62;
  then dom (f1/f2) = C;
  hence thesis by Def1;
end;

begin

::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::

Lm3: |.f.| is bounded iff f is bounded
proof
A1: dom f = dom |.f.| by VALUED_1:def 11;
  thus |.f.| is bounded implies f is bounded
  proof
    assume |.f.| is bounded;
    then consider r1 being Real such that
A2: for y st y in dom |.f.| holds |.abs(f).y.| < r1;
    take r1;
    let y;
    assume
A3: y in dom f;
    then |.abs(f).y.| < r1 by A1,A2;
    then |.|.f.y.|.| < r1 by A1,A3,VALUED_1:def 11;
    hence thesis;
  end;
  given r1 such that
A4: for y st y in dom f holds |.f.y.| <r1;
  now
    take r1;
    let y;
    assume
A5: y in dom |.f.|;
    then |.|.f.y.|.| <r1 by A1,A4;
    hence |.abs(f).y.| <r1 by A5,VALUED_1:def 11;
  end;
  hence thesis;
end;

theorem Th68:
  f|Y is bounded iff ex p be Real st for c st c in Y /\ dom
  f holds |.(f/.c).|<= p
proof
A1: dom |.f.| = dom f by VALUED_1:def 11;
A2: dom(|.f.||Y) = Y /\ dom|.f.| by RELAT_1:61;
A3: |.f.||Y = |.f|Y.| by RFUNCT_1:46;
  hereby
    assume f|Y is bounded;
    then |.f.||Y is bounded by A3,Lm3;
    then consider p be Real such that
A4: for c being object st c in dom(|.f.||Y) holds |.(|.f.||Y).c.| <= p
    by RFUNCT_1:72;
    now
      let c such that
A5:   c in Y /\ dom f;
      c in dom f by A5,XBOOLE_0:def 4;
      then
A6:   f.c = f/.c by PARTFUN1:def 6;
      |.(|.f.||Y).c.| = |.|.f.|.c.| by A1,A2,A5,FUNCT_1:47
        .= |.|.(f.c).|.| by VALUED_1:18;
      hence |.(f/.c).| <= p by A1,A2,A4,A5,A6;
    end;
    hence
    ex p be Real st for c st c in Y /\ dom f holds |.(f/.c).| <= p;
  end;
  given p be Real such that
A7: for c st c in Y /\ dom f holds |.(f/.c).| <= p;
A8: dom |.f.| = dom f by VALUED_1:def 11;
  now
    let c be object such that
A9: c in dom(|.f.||Y);
A10: c in dom |.f.| by A9,RELAT_1:57;
    |.(|.f.||Y).c.| = |.|.f.|.c.| by A9,FUNCT_1:47
      .= |.|.(f.c).|.| by VALUED_1:18
      .= |.|.(f/.c).|.| by A1,A10,PARTFUN1:def 6;
    hence |.(|.f.||Y).c.| <= p by A2,A7,A8,A9;
  end;
  then |.f.||Y is bounded by RFUNCT_1:72;
  hence thesis by A3,Lm3;
end;

theorem
  Y c= X & f|X is bounded implies f|Y is bounded
proof
  assume that
A1: Y c= X and
A2: f|X is bounded;
  |.f.||X = |.f|X.| by RFUNCT_1:46;
  then |.f.||X is bounded by A2,Lm3;
  then |.f.||Y = |.f|Y.| & |.f.||Y is bounded by A1,RFUNCT_1:46,74;
  hence thesis by Lm3;
end;

theorem
  X misses dom f implies f|X is bounded
proof
  assume X /\ dom f = {};
  then for c holds c in X /\ dom f implies |.(f/.c).| <= 0;
  hence thesis by Th68;
end;

theorem Th71:
  f|Y is bounded implies (r(#)f)|Y is bounded
proof
  assume
A1: f|Y is bounded;
  |.f.||Y = |.f|Y.| by RFUNCT_1:46;
  then |.f.||Y is bounded by A1,Lm3;
  then (|.r.|(#)|.f.|)|Y is bounded by RFUNCT_1:80;
  then |.r(#)f.||Y = |.(r(#)f)|Y.| & |.r(#)f.||Y is bounded by Th30,RFUNCT_1:46
;
  hence thesis by Lm3;
end;

theorem
  |.f.||X is bounded_below
proof
  now
    take z=0;
    let c be object;
A1: z <= |. f/.c .| by COMPLEX1:46;
    assume c in X /\ dom (|.f.|);
    then
A2: c in dom (|.f.|) by XBOOLE_0:def 4;
    dom |.f.| = dom f by VALUED_1:def 11;
    then f.c = f/.c by A2,PARTFUN1:def 6;
    hence z <= (|.f.|).c by A1,VALUED_1:18;
  end;
  hence thesis by RFUNCT_1:71;
end;

theorem Th73:
  f|Y is bounded implies |.f.||Y is bounded & (-f)|Y is bounded
proof
  assume
A1: f|Y is bounded;
  |.f.||Y = |.f|Y.| by RFUNCT_1:46;
  hence |.f.||Y is bounded by A1,Lm3;
  thus thesis by A1,Th71;
end;

theorem Th74:
  f1|X is bounded & f2|Y is bounded implies (f1+f2)|(X /\ Y) is bounded
proof
  assume that
A1: f1|X is bounded and
A2: f2|Y is bounded;
  consider r1 such that
A3: for c st c in X /\ dom f1 holds |.((f1/.c)).| <= r1 by A1,Th68;
  consider r2 such that
A4: for c st c in Y /\ dom f2 holds |.((f2/.c)).| <= r2 by A2,Th68;
  ex p1 st for c st c in X /\ Y /\ dom (f1+f2) holds |.(f1+f2)/.c.| <= p1
  proof
    take r0=r1+r2;
    let c;
A5: |.((f1/.c)) + ((f2/.c)).| <= |.((f1/.c)).|+|.((f2/.c)).| by COMPLEX1:56;
    assume
A6: c in X /\ Y /\ dom (f1+f2);
    then
A7: c in X /\ Y by XBOOLE_0:def 4;
    then
A8: c in X by XBOOLE_0:def 4;
A9: c in Y by A7,XBOOLE_0:def 4;
A10: c in dom (f1+f2) by A6,XBOOLE_0:def 4;
    then
A11: c in dom f1 /\ dom f2 by VALUED_1:def 1;
    then c in dom f2 by XBOOLE_0:def 4;
    then c in Y /\ dom f2 by A9,XBOOLE_0:def 4;
    then
A12: |.((f2/.c)).| <= r2 by A4;
    c in dom f1 by A11,XBOOLE_0:def 4;
    then c in X /\ dom f1 by A8,XBOOLE_0:def 4;
    then |.((f1/.c)).| <= r1 by A3;
    then |.((f1/.c)).|+|.((f2/.c)).| <= r0 by A12,XREAL_1:7;
    then |.((f1/.c)) + ((f2/.c)).| <= r0 by A5,XXREAL_0:2;
    hence thesis by A10,Th1;
  end;
  hence thesis by Th68;
end;

theorem Th75:
  f1|X is bounded & f2|Y is bounded implies (f1(#)f2)|(X /\ Y) is
  bounded & (f1-f2)|(X /\ Y) is bounded
proof
  assume that
A1: f1|X is bounded and
A2: f2|Y is bounded;
  consider r1 such that
A3: for c st c in X /\ dom f1 holds |.((f1/.c)).| <= r1 by A1,Th68;
  consider r2 such that
A4: for c st c in Y /\ dom f2 holds |.((f2/.c)).| <= r2 by A2,Th68;
  now
    take r=r1*r2;
    let c;
    assume
A5: c in X /\ Y /\ dom (f1(#)f2);
    then
A6: c in X /\ Y by XBOOLE_0:def 4;
    then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4;
    then
A9: c in dom f1 /\ dom f2 by Th3;
    then c in dom f1 by XBOOLE_0:def 4;
    then c in X /\ dom f1 by A7,XBOOLE_0:def 4;
    then
A10: |.((f1/.c)).| <= r1 by A3;
A11: c in Y by A6,XBOOLE_0:def 4;
    c in dom f2 by A9,XBOOLE_0:def 4;
    then c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
    then
A12: |.((f2/.c)).| <= r2 by A4;
    0<=|.((f1/.c)).| & 0<=|.((f2/.c)).| by COMPLEX1:46;
    then |.((f1/.c)).|*|.((f2/.c)).| <= r by A10,A12,XREAL_1:66;
    then |.((f1/.c)) * ((f2/.c)).| <= r by COMPLEX1:65;
    hence |.(f1(#)f2)/.c.| <= r by A8,Th3;
  end;
  hence (f1(#)f2)|(X /\ Y) is bounded by Th68;
  (-f2)|Y is bounded by A2,Th73;
  hence thesis by A1,Th74;
end;

theorem
  f|X is bounded & f|Y is bounded implies f|(X \/ Y) is bounded
proof
  assume that
A1: f|X is bounded and
A2: f|Y is bounded;
  |.f.||Y = |.f|Y.| by RFUNCT_1:46;
  then
A3: |.f.||Y is bounded by A2,Lm3;
  |.f.||X = |.f|X.| by RFUNCT_1:46;
  then |.f.||X is bounded by A1,Lm3;
  then |.f.||(X \/ Y) = |.f|(X \/ Y).| & |.f.||(X \/ Y) is bounded by A3,
RFUNCT_1:46,87;
  hence thesis by Lm3;
end;

theorem
  f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
  constant & (f1-f2)|(X /\ Y) is constant & (f1(#)f2)|(X /\ Y) is constant
proof
  assume that
A1: f1|X is constant and
A2: f2|Y is constant;
  consider cr1 being Element of COMPLEX such that
A3: for c st c in X /\ dom f1 holds (f1/.c) = cr1 by A1,PARTFUN2:35;
  consider cr2 being Element of COMPLEX such that
A4: for c st c in Y /\ dom f2 holds (f2/.c) = cr2 by A2,PARTFUN2:35;
A5: cr1 + cr2 in COMPLEX by XCMPLX_0:def 2;
  now
    let c;
    assume
A6: c in X /\ Y /\ dom (f1+f2);
    then
A7: c in X /\ Y by XBOOLE_0:def 4;
    then
A8: c in X by XBOOLE_0:def 4;
A9: c in dom (f1+f2) by A6,XBOOLE_0:def 4;
    then
A10: c in (dom f1 /\ dom f2) by VALUED_1:def 1;
    then c in dom f1 by XBOOLE_0:def 4;
    then
A11: c in X /\ dom f1 by A8,XBOOLE_0:def 4;
A12: c in Y by A7,XBOOLE_0:def 4;
    c in dom f2 by A10,XBOOLE_0:def 4;
    then
A13: c in Y /\ dom f2 by A12,XBOOLE_0:def 4;
    thus (f1+f2)/.c =((f1/.c)) + ((f2/.c)) by A9,Th1
      .= cr1 + ((f2/.c)) by A3,A11
      .= cr1 + cr2 by A4,A13;
  end;
  hence (f1+f2)|(X /\ Y) is constant by A5,PARTFUN2:35;
A14: cr1 - cr2 in COMPLEX by XCMPLX_0:def 2;
  now
    let c;
    assume
A15: c in X /\ Y /\ dom (f1-f2);
    then
A16: c in X /\ Y by XBOOLE_0:def 4;
    then
A17: c in X by XBOOLE_0:def 4;
A18: c in dom (f1-f2) by A15,XBOOLE_0:def 4;
    then
A19: c in (dom f1 /\ dom f2) by Th2;
    then c in dom f1 by XBOOLE_0:def 4;
    then
A20: c in X /\ dom f1 by A17,XBOOLE_0:def 4;
A21: c in Y by A16,XBOOLE_0:def 4;
    c in dom f2 by A19,XBOOLE_0:def 4;
    then
A22: c in Y /\ dom f2 by A21,XBOOLE_0:def 4;
    thus (f1-f2)/.c = ((f1/.c)) - ((f2/.c)) by A18,Th2
      .= cr1 - ((f2/.c)) by A3,A20
      .= cr1 - cr2 by A4,A22;
  end;
  hence (f1-f2)|(X /\ Y) is constant by A14,PARTFUN2:35;
A23: cr1 * cr2 in COMPLEX by XCMPLX_0:def 2;
  now
    let c;
    assume
A24: c in X /\ Y /\ dom (f1(#)f2);
    then
A25: c in X /\ Y by XBOOLE_0:def 4;
    then
A26: c in X by XBOOLE_0:def 4;
A27: c in dom (f1(#)f2) by A24,XBOOLE_0:def 4;
    then
A28: c in (dom f1 /\ dom f2) by Th3;
    then c in dom f1 by XBOOLE_0:def 4;
    then
A29: c in X /\ dom f1 by A26,XBOOLE_0:def 4;
A30: c in Y by A25,XBOOLE_0:def 4;
    c in dom f2 by A28,XBOOLE_0:def 4;
    then
A31: c in Y /\ dom f2 by A30,XBOOLE_0:def 4;
    thus (f1(#)f2)/.c =((f1/.c)) * ((f2/.c)) by A27,Th3
      .= cr1 * ((f2/.c)) by A3,A29
      .= cr1 * cr2 by A4,A31;
  end;
  hence thesis by A23,PARTFUN2:35;
end;

theorem Th78:
  f|Y is constant implies (q(#)f)|Y is constant
proof
  assume f|Y is constant;
  then consider r being Element of COMPLEX such that
A1: for c st c in Y /\ dom f holds (f/.c) = r by PARTFUN2:35;
A2: q*r in COMPLEX by XCMPLX_0:def 2;
  now
    let c;
    assume
A3: c in Y /\ dom (q(#)f);
    then
A4: c in Y by XBOOLE_0:def 4;
A5: c in dom (q(#)f) by A3,XBOOLE_0:def 4;
    then c in dom f by Th4;
    then
A6: c in Y /\ dom f by A4,XBOOLE_0:def 4;
    thus (q(#)f)/.c = q * (f/.c) by A5,Th4
      .= q*r by A1,A6;
  end;
  hence thesis by A2,PARTFUN2:35;
end;

theorem Th79:
  f|Y is constant implies |.f.||Y is constant & (-f)|Y is constant
proof
  assume f|Y is constant;
  then consider r being Element of COMPLEX such that
A1: for c st c in Y /\ dom f holds (f/.c) = r by PARTFUN2:35;
  reconsider rr= |.r.| as Element of REAL by XREAL_0:def 1;
  now
    let c;
    assume
A2: c in Y /\ dom (|.f.|);
    then c in dom (|.f.|) by XBOOLE_0:def 4;
    then
A3: c in dom f by VALUED_1:def 11;
    c in Y by A2,XBOOLE_0:def 4;
    then
A4: c in Y /\ dom f by A3,XBOOLE_0:def 4;
    f.c = f/.c by A3,PARTFUN1:def 6;
    hence (|.f.|).c = |.(f/.c).| by VALUED_1:18
      .= rr by A1,A4;
  end;
  hence |.f.||Y is constant by PARTFUN2:57;
A5: -r in COMPLEX by XCMPLX_0:def 2;
  now
    let c;
    assume
A6: c in Y /\ dom (-f);
    then c in Y /\ dom f by Th5;
    then
A7: -(f/.c) = -r by A1;
    c in dom (-f) by A6,XBOOLE_0:def 4;
    hence (-f)/.c = -r by A7,Th5;
  end;
  hence thesis by A5,PARTFUN2:35;
end;

theorem Th80:
  f|Y is constant implies f|Y is bounded
proof
  assume f|Y is constant;
  then consider r being Element of COMPLEX such that
A1: for c st c in Y /\ dom f holds (f/.c) = r by PARTFUN2:35;
  now
    take p=|.r.|;
    let c;
    assume c in Y /\ dom f;
    hence |.(f/.c).| <= p by A1;
  end;
  hence thesis by Th68;
end;

theorem
  f|Y is constant implies (for r holds (r(#)f)|Y is bounded) & (-f)|Y is
  bounded & |.f.||Y is bounded
proof
  assume
A1: f|Y is constant;
  hence for r holds (r(#)f)|Y is bounded by Th78,Th80;
  thus (-f)|Y is bounded by A1,Th79,Th80;
  |.f.||Y is constant by A1,Th79;
  hence thesis;
end;

theorem Th82:
  f1|X is bounded & f2|Y is constant implies (f1+f2)|(X /\ Y) is bounded
proof
  assume that
A1: f1|X is bounded and
A2: f2|Y is constant;
  f2|Y is bounded by A2,Th80;
  hence thesis by A1,Th74;
end;

theorem
  f1|X is bounded & f2|Y is constant implies (f1-f2)|(X /\ Y) is bounded
  & (f2-f1)|(X /\ Y) is bounded & (f1(#)f2)|(X /\ Y) is bounded
proof
  assume that
A1: f1|X is bounded and
A2: f2|Y is constant;
  (-f2)|Y is constant by A2,Th79;
  hence (f1-f2)|(X /\ Y) is bounded by A1,Th82;
A3: f2|Y is bounded by A2,Th80;
  hence (f2-f1)|(X /\ Y) is bounded by A1,Th75;
  thus thesis by A1,A3,Th75;
end;

theorem
  |.f.| is bounded iff f is bounded by Lm3;

registration let D be non empty set; let f be Function of COMPLEX,D;
 let c be Complex;
 identify f/.c with f.c;
 correctness
  proof
    reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
    f/.c = f.c by FUNCT_2:99;
   hence thesis;
  end; 
end;

theorem
  for f being complex-valued Function holds r(#)(-f) = -(r(#)f) by T2;