CFUNCDOM

:: Complex Valued Function's Space
::  by Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-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, FUNCT_2, NUMBERS, BINOP_1, FUNCT_1, BINOP_2,
      RELAT_1, ZFMISC_1, XCMPLX_0, FUNCOP_1, CARD_1, COMPLEX1, ARYTM_3,
      RLVECT_1, CLVECT_1, ARYTM_1, ALGSTR_0, SUPINF_2, CLOPBAN1, STRUCT_0,
      GROUP_1, MESFUNC1, FUNCSDOM, VECTSP_1, CFUNCDOM, VALUED_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
      FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, XCMPLX_0, VALUED_0,
      VALUED_2, BINOP_2, STRUCT_0, ALGSTR_0, RLVECT_1, COMPLEX1, GROUP_1,
      VECTSP_1, FUNCSDOM, CLVECT_1;
 constructors DOMAIN_1, BINOP_2, COMPLEX1, FUNCSDOM, CLVECT_1, VECTSP_1,
      RELSET_1, VALUED_2, VALUED_0, MEMBERED, NUMBERS, GROUP_1;
 registrations XBOOLE_0, RELSET_1, NUMBERS, VECTSP_1, CLVECT_1, XCMPLX_0,
      VALUED_2, MEMBERED;
 requirements SUBSET, BOOLE, ARITHM, NUMERALS;
 definitions RLVECT_1, STRUCT_0, GROUP_1, CLVECT_1, ALGSTR_0, VECTSP_1;
 equalities STRUCT_0, CLVECT_1, BINOP_1, ALGSTR_0;
 expansions RLVECT_1, STRUCT_0, GROUP_1, CLVECT_1, BINOP_1, VECTSP_1;
 theorems FUNCT_2, FUNCOP_1, RLVECT_1, VECTSP_1, TARSKI, COMPLEX1, BINOP_2,
      GROUP_1, ALGSTR_0, XCMPLX_0;
 schemes BINOP_1, FUNCT_2;

begin  :: Operation of complex functions

reserve x1,x2,z for set;
reserve A,B for non empty set;
reserve f,g,h for Element of Funcs(A,COMPLEX);

definition
  let A be set;
  func ComplexFuncAdd(A) -> BinOp of Funcs(A,COMPLEX) means
  :Def1:
  for f,g being Element of Funcs(A,COMPLEX) holds it.(f,g) = addcomplex.:(f,g);
  existence
  proof
    deffunc F(Element of Funcs(A,COMPLEX),Element of Funcs(A,COMPLEX)) =
    addcomplex.:($1,$2);
    consider F being BinOp of Funcs(A,COMPLEX) such that
A1: for x,y being Element of Funcs(A,COMPLEX) holds F.(x,y) = F(x,y)
    from BINOP_1:sch 4;
    take F;
    let f,g be Element of Funcs(A,COMPLEX);
    thus thesis by A1;
  end;
  uniqueness
  proof
    let it1,it2 be BinOp of Funcs(A,COMPLEX) such that
A2: for f,g being Element of Funcs(A,COMPLEX) holds it1.(f,g) =
    addcomplex.:(f,g) and
A3: for f,g being Element of Funcs(A,COMPLEX) holds it2.(f,g) =
    addcomplex.:(f,g);
    now
      let f,g be Element of Funcs(A,COMPLEX);
      thus it1.(f,g) = addcomplex.:(f,g) by A2
        .= it2.(f,g) by A3;
    end;
    hence thesis;
  end;
end;

registration let A be set;
 cluster ComplexFuncAdd A -> complex-functions-valued;
 coherence;
end;

definition
  let A be set;
  func ComplexFuncMult(A) -> BinOp of Funcs(A,COMPLEX) means
  :Def2:
  for f,g
  being Element of Funcs(A,COMPLEX) holds it.(f,g) = multcomplex.:(f,g);
  existence
  proof
    deffunc F(Element of Funcs(A,COMPLEX),Element of Funcs(A,COMPLEX)) =
    multcomplex.:($1,$2);
    consider F being BinOp of Funcs(A,COMPLEX) such that
A1: for x,y being Element of Funcs(A,COMPLEX) holds F.(x,y) = F(x,y)
    from BINOP_1:sch 4;
    take F;
    let f,g be Element of Funcs(A,COMPLEX);
    thus thesis by A1;
  end;
  uniqueness
  proof
    let it1,it2 be BinOp of Funcs(A,COMPLEX) such that
A2: for f,g being Element of Funcs(A,COMPLEX) holds it1.(f,g) =
    multcomplex.:(f,g) and
A3: for f,g being Element of Funcs(A,COMPLEX) holds it2.(f,g) =
    multcomplex.:(f,g);
    now
      let f,g be Element of Funcs(A,COMPLEX);
      thus it1.(f,g) = multcomplex.:(f,g) by A2
        .=it2.(f,g) by A3;
    end;
    hence thesis;
  end;
end;

registration let A be set;
 cluster ComplexFuncMult A -> complex-functions-valued;
 coherence;
end;

definition
  let A be non empty set;
  func ComplexFuncExtMult(A) ->
   Function of [:COMPLEX,Funcs(A,COMPLEX):], Funcs(A,COMPLEX) means
  :Def3:
  for z being Complex, f being Element of Funcs(A, COMPLEX),
      x being Element of A
     holds (it.[z,f]).x = z*(f.x);
  existence
  proof
    deffunc F(Element of COMPLEX,Element of Funcs(A,COMPLEX)) = (multcomplex
    [;]($1,$2));
    consider F being Function of [:COMPLEX,Funcs(A,COMPLEX):],Funcs(A,COMPLEX)
    such that
A1: for z being Element of COMPLEX, f being Element of Funcs(A,COMPLEX
    ) holds F.(z,f) = F(z,f) from BINOP_1:sch 4;
    take F;
    let z be Complex,
    f be Element of Funcs(A,COMPLEX), x be Element of A;
A2: z in COMPLEX by XCMPLX_0:def 2;
    then F.(z,f) = (multcomplex[;](z,f)) by A1;
    hence (F.[z,f]).x = multcomplex.(z,f.x) by FUNCOP_1:53,A2
      .= z*(f.x) by BINOP_2:def 5;
  end;
  uniqueness
  proof
    let it1,it2 be Function of [:COMPLEX,Funcs(A,COMPLEX):],Funcs(A,COMPLEX)
    such that
A3: for z being Complex, f being Element of Funcs(A,COMPLEX
    ), x being Element of A holds (it1.[z,f]).x = z*(f.x) and
A4: for z being Complex, f being Element of Funcs(A,COMPLEX
    ), x being Element of A holds (it2.[z,f]).x = z*(f.x);
    now
      let z be Element of COMPLEX, f be Element of Funcs(A,COMPLEX);
      now
        let x be Element of A;
        thus (it1.[z,f]).x = z*(f.x) by A3
          .= (it2.[z,f]).x by A4;
      end;
      hence it1.(z,f) = it2.(z,f) by FUNCT_2:63;
    end;
    hence thesis;
  end;
end;

registration let A be non empty set;
 cluster ComplexFuncExtMult A -> complex-functions-valued;
 coherence;
end;

definition
  let A;
  func ComplexFuncZero(A) -> Element of Funcs(A,COMPLEX) equals
  A --> 0;
  coherence
  proof
    A -->0c is Function of A,COMPLEX;
    hence thesis by FUNCT_2:8;
  end;
end;

definition
  let A;
  func ComplexFuncUnit(A) -> Element of Funcs(A,COMPLEX) equals
  A --> 1r;
  coherence by FUNCT_2:8;
end;

Lm1: for x being (Element of A), f being Function of A,B holds x in dom f
proof
  let x be (Element of A);
  let f be Function of A,B;
  x in A;
  hence thesis by FUNCT_2:def 1;
end;

theorem Th1:
  h = (ComplexFuncAdd(A)).(f,g) iff for x being Element of A holds
  h.x = f.x + g.x
proof
A1: now
    assume
A2: for x being Element of A holds h.x=f.x + g.x;
    now
      let x be Element of A;
A3:   x in dom (addcomplex.:(f,g)) by Lm1;
      thus ((ComplexFuncAdd(A)).(f,g)).x = (addcomplex.:(f,g)).x by Def1
        .= addcomplex.(f.x,g.x) by A3,FUNCOP_1:22
        .= f.x + g.x by BINOP_2:def 3
        .= h.x by A2;
    end;
    hence h = (ComplexFuncAdd(A)).(f,g) by FUNCT_2:63;
  end;
  now
    assume
A4: h = (ComplexFuncAdd(A)).(f,g);
    let x be Element of A;
A5: x in dom (addcomplex.:(f,g)) by Lm1;
    thus h.x = (addcomplex.:(f,g)).x by A4,Def1
      .= addcomplex.(f.x,g.x) by A5,FUNCOP_1:22
      .= f.x + g.x by BINOP_2:def 3;
  end;
  hence thesis by A1;
end;

theorem Th2:
  h = (ComplexFuncMult(A)).(f,g) iff for x being Element of A holds
  h.x = f.x * g.x
proof
A1: now
    assume
A2: for x being Element of A holds h.x=f.x * g.x;
    now
      let x be Element of A;
A3:   x in dom (multcomplex.:(f,g)) by Lm1;
      thus ((ComplexFuncMult(A)).(f,g)).x = (multcomplex.:(f,g)).x by Def2
        .= multcomplex.(f.x,g.x) by A3,FUNCOP_1:22
        .= f.x * g.x by BINOP_2:def 5
        .= h.x by A2;
    end;
    hence h = (ComplexFuncMult(A)).(f,g) by FUNCT_2:63;
  end;
  now
    assume
A4: h = (ComplexFuncMult(A)).(f,g);
    let x be Element of A;
A5: x in dom (multcomplex.:(f,g)) by Lm1;
    thus h.x = (multcomplex.:(f,g)).x by A4,Def2
      .= multcomplex.(f.x,g.x) by A5,FUNCOP_1:22
      .= f.x * g.x by BINOP_2:def 5;
  end;
  hence thesis by A1;
end;

theorem
  ComplexFuncZero(A) <> ComplexFuncUnit(A)
proof
  set a = the Element of A;
  (ComplexFuncZero(A)).a=0c by FUNCOP_1:7;
  hence thesis by COMPLEX1:def 4,FUNCOP_1:7;
end;

reserve a,b for Complex;

theorem Th4:
  h = (ComplexFuncExtMult(A)).[a,f] iff for x being Element of A
  holds h.x = a*(f.x)
proof
  thus h = (ComplexFuncExtMult(A)).[a,f] implies for x being Element of A
  holds h.x = a*(f.x) by Def3;
  reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
  now
    assume
A1: for x being Element of A holds h.x = a*(f.x);
    for x being Element of A holds h.x = ((ComplexFuncExtMult(A)).[a,f]).x
    proof
      let x be Element of A;
      thus h.x = a*(f.x) by A1
        .= ((ComplexFuncExtMult(A)).[a,f]).x by Def3;
    end;
    hence h = (ComplexFuncExtMult(A)).[a,f] by FUNCT_2:63;
  end;
  hence thesis;
end;

theorem Th5:
  (ComplexFuncAdd(A)).(f,g) = (ComplexFuncAdd(A)).(g,f)
proof
  now
    let x be Element of A;
    thus ((ComplexFuncAdd(A)).(f,g)).x = g.x + f.x by Th1
      .= ((ComplexFuncAdd(A)).(g,f)).x by Th1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th6:
  (ComplexFuncAdd(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
  ComplexFuncAdd(A)).((ComplexFuncAdd(A)).(f,g),h)
proof
  now
    let x be Element of A;
    thus ((ComplexFuncAdd(A)).(f,(ComplexFuncAdd(A)).(g,h))).x = f.x + ((
    ComplexFuncAdd(A)).(g,h)).x by Th1
      .= f.x + (g.x + h.x) by Th1
      .= (f.x + g.x) + h.x
      .= ((ComplexFuncAdd(A)).(f,g)).x + h.x by Th1
      .= ((ComplexFuncAdd(A)).((ComplexFuncAdd(A)).(f,g),h)).x by Th1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th7:
  (ComplexFuncMult(A)).(f,g) = (ComplexFuncMult(A)).(g,f)
proof
  now
    let x be Element of A;
    thus ((ComplexFuncMult(A)).(f,g)).x = g.x * f.x by Th2
      .= ((ComplexFuncMult(A)).(g,f)).x by Th2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th8:
  (ComplexFuncMult(A)).(f,(ComplexFuncMult(A)).(g,h)) = (
  ComplexFuncMult(A)).((ComplexFuncMult(A)).(f,g),h)
proof
  now
    let x be Element of A;
    thus ((ComplexFuncMult(A)).(f,(ComplexFuncMult(A)).(g,h))).x = f.x * ((
    ComplexFuncMult(A)).(g,h)).x by Th2
      .= f.x * (g.x * h.x) by Th2
      .= (f.x * g.x) * h.x
      .= ((ComplexFuncMult(A)).(f,g)).x * h.x by Th2
      .= ((ComplexFuncMult(A)).((ComplexFuncMult(A)).(f,g),h)).x by Th2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th9:
  (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) = f
proof
  now
    let x be Element of A;
    thus ((ComplexFuncMult(A)).(ComplexFuncUnit(A),f)).x= (ComplexFuncUnit(A))
    .x * f.x by Th2
      .=1r * f.x by FUNCOP_1:7
      .= f.x by COMPLEX1:def 4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th10:
  (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) = f
proof
  now
    let x be Element of A;
    thus ((ComplexFuncAdd(A)).(ComplexFuncZero(A),f)).x = (ComplexFuncZero(A))
    .x + f.x by Th1
      .= 0c + f.x by FUNCOP_1:7
      .= f.x;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th11:
  (ComplexFuncAdd(A)).(f,(ComplexFuncExtMult(A)).[-1r,f]) = ComplexFuncZero(A)
proof
  reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
  now
    let x be Element of A;
    set y=f.x;
    thus ((ComplexFuncAdd(A)).(f,(ComplexFuncExtMult(A)).[mj,f])).x
     = f.x + ((ComplexFuncExtMult(A)).[mj,f]).x by Th1
      .= f.x + (mj*y) by Th4
      .= (ComplexFuncZero(A)).x by COMPLEX1:def 4,FUNCOP_1:7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th12:
  (ComplexFuncExtMult(A)).[1r,f] = f
proof
  now
    let x be Element of A;
    thus ((ComplexFuncExtMult(A)).[1r,f]).x = 1r*(f.x) by Th4
      .= f.x by COMPLEX1:def 4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th13:
  for a, b be Complex holds
  (ComplexFuncExtMult(A)).[a,(ComplexFuncExtMult(A)).[b,f]] = (
  ComplexFuncExtMult(A)).[a*b,f]
proof
  let a, b be Complex;
  reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
  reconsider ab = a*b as Element of COMPLEX by XCMPLX_0:def 2;
  now
    let x be Element of A;
    thus ((ComplexFuncExtMult(A)).[a,(ComplexFuncExtMult(A)).[b,f]]).x = a*(((
    ComplexFuncExtMult(A)).[b,f]).x) by Th4
      .= a*(b*(f.x)) by Th4
      .= (a*b)*(f.x)
      .= ((ComplexFuncExtMult(A)).[ab,f]).x by Th4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th14:
  for a, b be Complex holds
  (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,f]) = (ComplexFuncExtMult(A)).[a+b,f]
proof
  let a, b be Complex;
  reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;
  reconsider ab = a+b as Element of COMPLEX by XCMPLX_0:def 2;
  now
    let x be Element of A;
    thus ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
    ComplexFuncExtMult(A)).[b,f])).x = ((ComplexFuncExtMult(A)).[a,f]).x + ((
    ComplexFuncExtMult(A)).[b,f]).x by Th1
      .= a*(f.x) + ((ComplexFuncExtMult(A)).[b,f]).x by Th4
      .= a*(f.x) + b*(f.x) by Th4
      .= (a+b)*(f.x)
      .= ((ComplexFuncExtMult(A)).[ab,f]).x by Th4;
  end;
  hence thesis by FUNCT_2:63;
end;

Lm2:
    for a be Complex holds
    (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A
)).[a,g]) = (ComplexFuncExtMult(A)).[a,(ComplexFuncAdd(A)).(f,g)]
proof
  let a be Complex;
  reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
  now
    let x be Element of A;
    thus ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
    ComplexFuncExtMult(A)).[a,g])).x = ((ComplexFuncExtMult(A)).[a,f]).x + ((
    ComplexFuncExtMult(A)).[a,g]).x by Th1
      .= a*(f.x) + ((ComplexFuncExtMult(A)).[a,g]).x by Th4
      .= a*(f.x) + a*(g.x) by Th4
      .= a*(f.x + g.x)
      .= a*(((ComplexFuncAdd(A)).(f,g)).x) by Th1
      .= ((ComplexFuncExtMult(A)).[a,(ComplexFuncAdd(A)).(f,g)]).x by Th4;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th15:
  (ComplexFuncMult(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
  ComplexFuncAdd(A)).((ComplexFuncMult(A)).(f,g),(ComplexFuncMult(A)).(f,h))
proof
  now
    let x be Element of A;
    thus ((ComplexFuncMult(A)).(f,(ComplexFuncAdd(A)).(g,h))).x = f.x * (((
    ComplexFuncAdd(A)).(g,h)).x) by Th2
      .= f.x * (g.x + h.x) by Th1
      .= (f.x * g.x) + (f.x * h.x)
      .= ((ComplexFuncMult(A)).(f,g)).x + (f.x * h.x) by Th2
      .= ((ComplexFuncMult(A)).(f,g)).x + ((ComplexFuncMult(A)).(f,h)).x by Th2
      .= ((ComplexFuncAdd(A)). ((ComplexFuncMult(A)).(f,g),(ComplexFuncMult(
    A)).(f,h))).x by Th1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  (ComplexFuncMult(A)).((ComplexFuncExtMult(A)).[a,f],g) = (
  ComplexFuncExtMult(A)).[a,(ComplexFuncMult(A)).(f,g)]
proof
  reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
  now
    let x be Element of A;
    thus ((ComplexFuncMult(A)).((ComplexFuncExtMult(A)).[a,f],g)).x
       = ((ComplexFuncExtMult(A)).[a,f]).x * g.x by Th2
      .= (a*(f.x)) * g.x by Th4
      .= a*(f.x * g.x)
      .= a*(((ComplexFuncMult(A)).(f,g)).x) by Th2
      .= ((ComplexFuncExtMult(A)).[a,(ComplexFuncMult(A)).(f,g)]).x
           by Th4;
  end;
  hence thesis by FUNCT_2:63;
end;

begin  :: Complex linear space of complex valued functions

theorem Th17:
  ex f,g st (for z st z in A holds (z = x1 implies f.z = 1r) & (z
<>x1 implies f.z = 0)) & for z st z in A holds (z = x1 implies g.z = 0) & (z<>
  x1 implies g.z = 1r)
proof
  deffunc G(object) = 1r;
  deffunc F(object) = 0c;
  defpred P[object] means $1 = x1;
A1: for z being object st z in A
holds (P[z] implies G(z) in COMPLEX) & (not P[z] implies
  F(z) in COMPLEX);
  consider f being Function of A,COMPLEX such that
A2: for z being object st z in A
 holds (P[z] implies f.z = G(z)) & (not P[z] implies
  f.z = F(z)) from FUNCT_2:sch 5(A1);
A3: for z being object st z in A
holds (P[z] implies F(z) in COMPLEX) & (not P[z] implies
  G(z) in COMPLEX);
  consider g being Function of A,COMPLEX such that
A4: for z being object st z in A
holds (P[z] implies g.z = F(z)) & (not P[z] implies
  g.z = G(z)) from FUNCT_2:sch 5(A3);
  reconsider f,g as Element of Funcs(A,COMPLEX) by FUNCT_2:8;
  take f,g;
  thus thesis by A2,A4;
end;

theorem Th18:
  x1 in A & x2 in A & x1<>x2 & (for z st z in A holds (z=x1
  implies f.z = 1r) & (z<>x1 implies f.z = 0)) & (for z st z in A holds (z=x1
implies g.z = 0) & (z<>x1 implies g.z = 1r)) implies for a,b st (ComplexFuncAdd
  (A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g]) =
  ComplexFuncZero(A) holds a=0c & b=0c
proof
  assume that
A1: x1 in A and
A2: x2 in A and
A3: x1<>x2 and
A4: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1r);
A5: f.x2=0c & g.x2=1r by A2,A3,A4;
A6: f.x1=1r & g.x1=0c by A1,A4;
  let a,b;
  reconsider x1,x2 as Element of A by A1,A2;
  assume
A7: (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A);
  reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
A8: 0c = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,g])).x2 by FUNCOP_1:7,A7
    .= (((ComplexFuncExtMult(A)).[a,f]).x2) + (((ComplexFuncExtMult(A)).[b,g
  ]).x2) by Th1
    .= a*(f.x2) + (((ComplexFuncExtMult(A)).[b,g]).x2) by Th4
    .= 0c + b*1r by A5,Th4
    .= b by COMPLEX1:def 4;
  0c = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,g])).x1 by A7,FUNCOP_1:7
    .= (((ComplexFuncExtMult(A)).[a,f]).x1) + (((ComplexFuncExtMult(A)).[b,g
  ]).x1) by Th1
    .= a*(f.x1) + (((ComplexFuncExtMult(A)).[b,g]).x1) by Th4
    .= a + b*0c by A6,Th4,COMPLEX1:def 4
    .= a;
  hence thesis by A8;
end;

theorem
  x1 in A & x2 in A & x1<>x2 implies ex f,g st for a,b st (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ]) = ComplexFuncZero(A) holds a=0 & b=0
proof
  assume
A1: x1 in A & x2 in A & x1<>x2;
  consider f,g such that
A2: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r
  ) by Th17;
  take f,g;
  let a,b;
  assume (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A);
  hence thesis by A1,A2,Th18;
end;

theorem Th20:
  A = {x1,x2} & x1<>x2 & ( for z st z in A holds (z=x1 implies f.z
= 1r) & (z<>x1 implies f.z = 0) ) & ( for z st z in A holds (z=x1 implies g.z =
  0) & (z<>x1 implies g.z = 1r) ) implies for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ])
proof
  assume that
A1: A = {x1,x2} and
A2: x1<>x2 and
A3: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1r);
  x2 in A by A1,TARSKI:def 2;
  then
A4: f.x2=0c & g.x2=1r by A2,A3;
  x1 in A by A1,TARSKI:def 2;
  then
A5: f.x1=1r & g.x1=0c by A3;
  let h;
  reconsider x1,x2 as Element of A by A1,TARSKI:def 2;
  take a = h.x1, b = h.x2;
  now
    let x be Element of A;
A6: x = x1 or x = x2 by A1,TARSKI:def 2;
A7: ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x2 = (((ComplexFuncExtMult(A)).[a,f]).x2) + (((
    ComplexFuncExtMult(A)).[b,g]).x2) by Th1
      .= a*(f.x2) + (((ComplexFuncExtMult(A)).[b,g]).x2) by Th4
      .= 0c + b*1r by A4,Th4
      .= h.x2 by COMPLEX1:def 4;
    ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x1 = (((ComplexFuncExtMult(A)).[a,f]).x1) + (((
    ComplexFuncExtMult(A)).[b,g]).x1) by Th1
      .= a*(f.x1) + (((ComplexFuncExtMult(A)).[b,g]).x1) by Th4
      .= a + b*0c by A5,Th4,COMPLEX1:def 4
      .= h.x1;
    hence h.x = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
    ComplexFuncExtMult(A)).[b,g])).x by A6,A7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  A = {x1,x2} & x1<>x2 implies ex f,g st for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ])
proof
  assume
A1: A = {x1,x2} & x1<>x2;
  consider f,g such that
A2: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
=0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r)
  by Th17;
  take f,g;
  let h;
  thus thesis by A1,A2,Th20;
end;

theorem Th22:
  A = {x1,x2} & x1<>x2 implies ex f,g st (for a,b st (
ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (ComplexFuncExtMult(A)).[b,g
  ]) = ComplexFuncZero(A) holds a=0 & b=0) & for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ])
proof
  assume that
A1: A = {x1,x2} and
A2: x1<>x2;
  consider f,g such that
A3: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
=0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r)
  by Th17;
  take f,g;
  x1 in A & x2 in A by A1,TARSKI:def 2;
  hence thesis by A1,A2,A3,Th18,Th20;
end;

definition
  let A;
  func ComplexVectSpace(A) -> strict non empty CLSStruct equals
  CLSStruct(# Funcs(A,COMPLEX), ComplexFuncZero A,
              ComplexFuncAdd A, ComplexFuncExtMult A #);
  coherence;
end;

reserve C for strict non empty CLSStruct,
        u,v,w for Element of C;

registration
  let A;
  cluster ComplexVectSpace A -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital for strict non empty CLSStruct;
  coherence
  proof let C such that
A1:  C = ComplexVectSpace A;
   thus u+v = v+u by Th5,A1;
   thus (u + v) + w = u + (v + w) by Th6,A1;
   thus u+0.C = u
     proof
       reconsider v=u as Element of Funcs(A,COMPLEX) by A1;
       thus u+0.C = (ComplexFuncAdd(A)).(ComplexFuncZero(A),v) by Th5,A1
         .= u by Th10;
     end;
   thus u is right_complementable
    proof
      reconsider v = u as Element of Funcs(A,COMPLEX) by A1;
      reconsider mj = -1r as Element of  COMPLEX by XCMPLX_0:def 2;
      reconsider w = (ComplexFuncExtMult(A)).[mj,v] as VECTOR of C by A1;
        take w;
        thus thesis by Th11,A1;
      end;
   thus for a be Complex, u,v be VECTOR of C holds a * (u + v) = a*u + a*v
   by Lm2,A1;
   thus for a,b be Complex, v be VECTOR of C holds (a+b)*v = a*v + b*v
   by Th14,A1;
   thus for a,b be Complex, v be VECTOR of C holds (a*b)*v = a*(b*v) by Th13,A1
;
   thus 1r * v = v by Th12,A1;
  end;
end;

Lm3: ex A,x1,x2 st A={x1,x2} & x1<>x2
proof
  reconsider A={1,2} as non empty set;
  take A;
  thus thesis;
end;

theorem
  ex V being strict ComplexLinearSpace st ex u,v being VECTOR of V st (
  for a,b st a*u + b*v = 0.V holds a=0 & b=0) & for w being VECTOR of V
  ex a,b st w = a*u + b*v
proof
  consider A,x1,x2 such that
A1: A={x1,x2} & x1<>x2 by Lm3;
  take V = ComplexVectSpace(A);
  consider f,g such that
A2: for a,b st (ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (
  ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A) holds a=0c & b=0c and
A3: for h holds ex a,b st h = (ComplexFuncAdd(A)). ((ComplexFuncExtMult(
  A)).[a,f],(ComplexFuncExtMult(A)).[b,g]) by A1,Th22;
  reconsider u=f, v=g as VECTOR of V;
  take u,v;
  thus for a,b st a*u + b*v = 0.V holds a=0 & b=0 by A2;
  thus for w being VECTOR of V ex a,b st w = a*u + b*v
  proof
    let w be VECTOR of V;
    reconsider h=w as Element of Funcs(A,COMPLEX);
    consider a,b such that
A4: h = (ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (
    ComplexFuncExtMult(A)).[b,g]) by A3;
    h = a*u + b*v by A4;
    hence thesis;
  end;
end;

definition
  let A;
  func CRing(A) -> doubleLoopStr equals
  doubleLoopStr(# Funcs(A,COMPLEX), ComplexFuncAdd A, ComplexFuncMult A,
       ComplexFuncUnit A, ComplexFuncZero A #);
  correctness;
end;

registration
  let A;
  cluster CRing A -> non empty strict;
  coherence;
end;

Lm4: now
  let A;
  let x, e be Element of CRing(A);
  assume e = ComplexFuncUnit(A);
  hence e * x = x by Th9;
  hence x * e = x by Th7;
end;

registration
  let A;
  cluster CRing(A) -> unital;
  coherence
  proof
    reconsider e = ComplexFuncUnit(A) as Element of CRing(A);
    take e;
    thus thesis by Lm4;
  end;
end;

theorem Th24:
  for x,y,z being Element of CRing(A) holds x+y = y+x & (x+y)+z =
x+(y+z) & x+(0.CRing(A)) = x & x is right_complementable & x*y = y*x & (x*y)*z
= x*(y*z) & x*(1.CRing(A)) = x & (1.CRing(A))*x = x & x*(y+z) = x*y + x*z & (y+
  z)*x = y*x + z*x
proof
  let x,y,z be Element of CRing(A);
  set IT = CRing(A);
  reconsider f=x as Element of Funcs(A,COMPLEX);
  thus x+y = y+x by Th5;
  thus (x+y)+z = x+(y+z) by Th6;
  thus x+(0.CRing(A)) = (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) by Th5
    .= x by Th10;
  thus ex t being Element of CRing(A) st x+t=(0.CRing(A))
  proof
    reconsider mj=-1r as Element of COMPLEX by XCMPLX_0:def 2;
    set h = (ComplexFuncExtMult(A)).[mj,f];
    reconsider t=h as Element of IT;
    take t;
    thus thesis by Th11;
  end;
  thus x*y = y*x by Th7;
  thus (x*y)*z = x*(y*z) by Th8;
  thus x*(1.CRing(A)) = (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) by Th7
    .= x by Th9;
  hence (1.CRing(A))*x = x by Th7;
  thus x*(y+z) = x*y + x*z by Th15;
  hence (y+z)*x = x*y + x*z by Th7
    .= y*x + x*z by Th7
    .= y*x + z*x by Th7;
end;

theorem
  CRing(A) is commutative Ring
proof
  for x,y,z being Element of CRing(A) holds x+y = y+x & (x+y)+z = x+(y+z)
& x+(0.CRing(A)) = x & x is right_complementable & x*y = y*x & (x*y)*z = x*(y*z
) & x*(1.CRing(A)) = x & (1.CRing(A))*x = x & x*(y+z) = x*y + x*z & (y+z)*x = y
  *x + z*x by Th24;
  hence thesis by ALGSTR_0:def 16,GROUP_1:def 3,def 12,RLVECT_1:def 2,def 3
,def 4,VECTSP_1:def 6,def 7;
end;

definition
  struct(doubleLoopStr,CLSStruct) ComplexAlgebraStr (# carrier -> set, multF,
addF -> (BinOp of the carrier), Mult -> (Function of [:COMPLEX,the carrier:],
    the carrier), OneF,ZeroF -> Element of the carrier #);
end;

registration
  cluster non empty for ComplexAlgebraStr;
  existence
  proof

set X = the non empty set,m = the BinOp of X,M = the Function of [:COMPLEX,X:],
X,u = the Element of X;
    take ComplexAlgebraStr(#X,m,m,M,u,u#);
    thus the carrier of ComplexAlgebraStr(#X,m,m,M,u,u#) is non empty;
  end;
end;

definition
  let A;
  func CAlgebra(A) -> strict ComplexAlgebraStr equals
  ComplexAlgebraStr(#Funcs
    (A,COMPLEX),ComplexFuncMult(A),ComplexFuncAdd(A), ComplexFuncExtMult(A),(
    ComplexFuncUnit(A)),(ComplexFuncZero(A))#);
  correctness;
end;

registration
  let A;
  cluster CAlgebra(A) -> non empty;
  coherence;
end;

Lm5: now
  let A;
  let x, e be Element of CAlgebra(A);
  assume e = ComplexFuncUnit(A);
  hence e * x = x by Th9;
  hence x * e = x by Th7;
end;

registration
  let A;
  cluster CAlgebra(A) -> unital;
  coherence
  proof
    reconsider e = ComplexFuncUnit(A) as Element of CAlgebra(A);
    take e;
    thus thesis by Lm5;
  end;
end;

theorem
  for x,y,z being Element of CAlgebra(A), a,b holds x + y = y + x
  & (x + y) + z = x + (y + z) & x + (0.CAlgebra(A)) = x & x is
  right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1.
CAlgebra(A)) = x & x * (y + z) = x * y + x * z & a * (x * y) = (a * x) * y & a
* (x + y) = a * x + a * y & (a + b) * x = a * x + b * x & (a * b) * x = a * (b
  * x)
proof
  let x,y,z be Element of CAlgebra(A);
  let a,b;
  set IT = CAlgebra(A);
  reconsider f=x as Element of Funcs(A,COMPLEX);
  thus x+y = y+x by Th5;
  thus (x+y)+z = x+(y+z) by Th6;
  thus x+(0.CAlgebra(A)) = (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) by Th5
    .= x by Th10;
  thus ex t being Element of CAlgebra(A) st x+t=(0.CAlgebra(A))
  proof
    reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
    set h = (ComplexFuncExtMult(A)).[mj,f];
    reconsider t=h as Element of IT;
    take t;
    thus thesis by Th11;
  end;
  thus x*y = y*x by Th7;
  thus (x*y)*z = x*(y*z) by Th8;
  thus x*(1.CAlgebra(A)) = (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) by Th7
    .= x by Th9;
  thus x*(y+z) = x*y + x*z by Th15;
  thus a*(x*y) = (a*x)*y by Th16;
  thus a*(x+y) = (a*x) + (a*y) by Lm2;
  thus (a+b)*x = (a*x) + (b*x) by Th14;
  thus thesis by Th13;
end;

definition
  let IT be non empty ComplexAlgebraStr;
  attr IT is vector-associative means
 for x,y being Element of IT, a holds a * (x * y) = (a * x) * y;
end;

registration let A;
 cluster CAlgebra A -> strict Abelian add-associative right_zeroed
      right_complementable commutative associative right_unital
      right-distributive vector-distributive scalar-distributive
      scalar-associative vector-associative;
 coherence
  proof set C = CAlgebra A;
   thus C is strict;
   thus C is Abelian by Th5;
   thus C is add-associative by Th6;
   thus C is right_zeroed proof let x be Element of C;
      reconsider f=x as Element of Funcs(A,COMPLEX);
     thus x+0.C = (ComplexFuncAdd A).(ComplexFuncZero A,f) by Th5
         .= x by Th10;
    end;
   thus C is right_complementable proof let x be Element of C;
    reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
      reconsider f=x as Element of Funcs(A,COMPLEX);
      reconsider t=(ComplexFuncExtMult A).[mj,f] as Element of C;
     take t;
     thus thesis by Th11;
    end;
   thus C is commutative by Th7;
   thus C is associative by Th8;
   thus C is right_unital proof let x be Element of C;
      reconsider f=x as Element of Funcs(A,COMPLEX);
     thus x* 1.C = (ComplexFuncMult A).(ComplexFuncUnit A,f) by Th7
    .= x by Th9;
    end;
   thus C is right-distributive by Th15;
   thus C is vector-distributive by Lm2;
   thus C is scalar-distributive by Th14;
   thus C is scalar-associative by Th13;
   let x,y be Element of C; let a;
   thus thesis by Th16;
  end;
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
    commutative associative right_unital right-distributive vector-distributive
    scalar-distributive scalar-associative vector-associative
     for non empty ComplexAlgebraStr;
  existence
  proof
   take CAlgebra {0};
   thus thesis;
  end;
end;

definition
  mode ComplexAlgebra is Abelian add-associative right_zeroed
    right_complementable commutative associative right_unital
    right-distributive vector-distributive scalar-distributive
    scalar-associative vector-associative non empty ComplexAlgebraStr;
end;

theorem
  CAlgebra(A) is ComplexAlgebra;

theorem
  1.CRing(A) = ComplexFuncUnit(A);

theorem
  1.CAlgebra(A) = ComplexFuncUnit(A);