:: Real Functions Spaces
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received March 23, 1990
:: Copyright (c) 1990-2012 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, BINOP_1, FUNCT_2, SUBSET_1, FUNCT_1, ZFMISC_1, NUMBERS,
      RELAT_1, FUNCOP_1, BINOP_2, REAL_1, CARD_1, ARYTM_3, RLVECT_1, ARYTM_1,
      STRUCT_0, ALGSTR_0, XREAL_0, ORDINAL1, SUPINF_2, GROUP_1, MESFUNC1,
      VECTSP_1, LATTICES, FUNCSDOM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, BINOP_2, ORDINAL1, XCMPLX_0,
      XREAL_0, STRUCT_0, ALGSTR_0, RLVECT_1, REAL_1, GROUP_1, VECTSP_1;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, BINOP_2, VECTSP_1, RLVECT_1,
      FUNCT_3, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, RLVECT_1, VECTSP_1,
      ALGSTR_0, BINOP_2, FUNCOP_1, FUNCT_3, REAL_1, XREAL_0, ORDINAL1, RELAT_1,
      VALUED_0, STRUCT_0, CARD_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions RLVECT_1, STRUCT_0, GROUP_1, BINOP_1, VECTSP_1, ALGSTR_0,
      FUNCOP_1, FUNCT_2;
 theorems FUNCT_2, BINOP_1, FUNCOP_1, TARSKI, BINOP_2, STRUCT_0, XREAL_0;
 schemes BINOP_1, FUNCT_2;

begin

reserve x1,x2,z for set;
reserve A,B for non empty set;

definition
  let A be set, B be non empty set;
  let F be BinOp of Funcs(A,B);
  let f,g be Element of Funcs(A,B);
  redefine func F.(f,g) -> Element of Funcs(A,B);
  coherence
  proof
    reconsider f,g as Element of Funcs(A,B) qua non empty set;
    F.(f,g) is Element of Funcs(A,B);
    hence thesis;
  end;
end;

definition
  let A,B,C,D be non empty set;
  let F be Function of [:C,D:],Funcs(A,B);
  let cd be Element of [:C,D:];
  redefine func F.cd -> Element of Funcs(A,B);
  coherence
  proof
    F.cd is Element of Funcs(A,B);
    hence thesis;
  end;
end;

reserve f,g,h for Element of Funcs(A,REAL);

definition
  let X be non empty set, Z be set;
  let F be (BinOp of X), f,g be Function of Z,X;

  redefine func F.:(f,g) -> Element of Funcs(Z,X);
  coherence
  proof
    F.:(f,g) in Funcs(Z,X) by FUNCT_2:8;
    hence thesis;
  end;
end;

definition
  let X be non empty set, Z be set;
  let F be (BinOp of X),a be Element of X,f be Function of Z,X;
  redefine func F[;](a,f) -> Element of Funcs(Z,X);
  coherence
  proof
    F[;](a,f) in Funcs(Z,X) by FUNCT_2:8;
    hence thesis;
  end;
end;

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

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

definition let A be set;
  func RealFuncExtMult(A) -> Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL)
  means
  :Def3:
  for a being Real, f being Element of Funcs(A,REAL) holds it.(a,f)
  = multreal[;](a,f);
  existence
  proof
    deffunc F(Element of REAL,Element of Funcs(A,REAL)) = (multreal[;]($1,$2));
    consider F being Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL) such
    that
A1: for a being Element of REAL, f being Element of Funcs(A,REAL)
    holds F.(a,f) = F(a,f) from BINOP_1:sch 4;
    take F;
    let a be Real, f be Element of Funcs(A,REAL);
    thus thesis by A1;
  end;
  uniqueness
  proof
    let it1,it2 be Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL) such that
A2: for a being Real, f being Element of Funcs(A,REAL) holds it1.(a,f)
    = multreal[;](a,f) and
A3: for a being Real, f being Element of Funcs(A,REAL) holds it2.(a,f)
    = multreal[;](a,f);
    now
      let a be Real, f be Element of Funcs(A,REAL);
      thus it1.(a,f) = multreal[;](a,f) by A2
        .= it2.(a,f) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let A be set;
  func RealFuncZero A -> Element of Funcs(A,REAL) equals
  A --> 0;
  coherence
  proof
    A --> 0 is Function of A,REAL by FUNCOP_1:45;
    hence thesis by FUNCT_2:8;
  end;
end;

definition
  let A be set;
  func RealFuncUnit A -> Element of Funcs(A,REAL) equals
  A --> 1;
  coherence
  proof
    A --> 1 is Function of A,REAL by FUNCOP_1:45;
    hence thesis by FUNCT_2:8;
  end;
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),f be Function of A,B;
  x in A;
  hence thesis by FUNCT_2:def 1;
end;

theorem Th1:
  h = (RealFuncAdd 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 (addreal.:(f,g)) by Lm1;
      thus ((RealFuncAdd A).(f,g)).x = (addreal.:(f,g)).x by Def1
        .= addreal.(f.x,g.x) by A3,FUNCOP_1:22
        .= f.x + g.x by BINOP_2:def 9
        .= h.x by A2;
    end;
    hence h = (RealFuncAdd A).(f,g) by FUNCT_2:63;
  end;
  now
    assume
A4: h = (RealFuncAdd A).(f,g);
    let x be Element of A;
A5: x in dom (addreal.:(f,g)) by Lm1;
    thus h.x = (addreal.:(f,g)).x by A4,Def1
      .= addreal.(f.x,g.x) by A5,FUNCOP_1:22
      .= f.x + g.x by BINOP_2:def 9;
  end;
  hence thesis by A1;
end;

theorem Th2:
  h = (RealFuncMult(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 (multreal.:(f,g)) by Lm1;
      thus ((RealFuncMult(A)).(f,g)).x = (multreal.:(f,g)).x by Def2
        .= multreal.(f.x,g.x) by A3,FUNCOP_1:22
        .= f.x * g.x by BINOP_2:def 11
        .= h.x by A2;
    end;
    hence h = (RealFuncMult(A)).(f,g) by FUNCT_2:63;
  end;
  now
    assume
A4: h = (RealFuncMult(A)).(f,g);
    let x be Element of A;
A5: x in dom (multreal.:(f,g)) by Lm1;
    thus h.x = (multreal.:(f,g)).x by A4,Def2
      .= multreal.(f.x,g.x) by A5,FUNCOP_1:22
      .= f.x * g.x by BINOP_2:def 11;
  end;
  hence thesis by A1;
end;

theorem
  RealFuncZero(A) <> RealFuncUnit(A)
proof
  set a = the Element of A;
  (RealFuncZero(A)).a=0 by FUNCOP_1:7;
  hence thesis by FUNCOP_1:7;
end;

reserve a,b for Real;

theorem Th4:
  h = (RealFuncExtMult A).[a,f] iff for x being Element of A holds
  h.x = a*(f.x)
proof
  thus h = (RealFuncExtMult A).[a,f] implies for x being Element of A holds h.
  x = a*(f.x)
  proof
    assume
A1: h = (RealFuncExtMult A).[a,f];
    let x be Element of A;
    h = (RealFuncExtMult A).(a,f) by A1;
    hence h.x = (multreal[;](a,f)).x by Def3
      .= multreal.(a,f.x) by FUNCOP_1:53
      .= a*(f.x) by BINOP_2:def 11;
  end;
  now
    assume
A2: for x being Element of A holds h.x = a*(f.x);
    for x being Element of A holds h.x = ((RealFuncExtMult A).[a,f]).x
    proof
      let x be Element of A;
A3:   multreal[;](a,f) = (RealFuncExtMult A).(a,f) by Def3;
      thus h.x = a*(f.x) by A2
        .= multreal.(a,f.x) by BINOP_2:def 11
        .= ((RealFuncExtMult A).[a,f]).x by A3,FUNCOP_1:53;
    end;
    hence h = (RealFuncExtMult A).(a,f) by FUNCT_2:63;
  end;
  hence thesis;
end;

theorem Th5:
  for A being set, f,g being Element of Funcs(A,REAL) holds (
  RealFuncAdd A).(f,g) = (RealFuncAdd A).(g,f)
proof
  let A be set, f,g be Element of Funcs(A,REAL);
  thus (RealFuncAdd A).(f,g) = addreal.:(f,g) by Def1
    .= addreal.:(g,f) by FUNCOP_1:65
    .= (RealFuncAdd A).(g,f) by Def1;
end;

theorem Th6:
  for A being set, f,g,h being Element of Funcs(A,REAL) holds (
RealFuncAdd A).(f,(RealFuncAdd A).(g,h)) = (RealFuncAdd A).((RealFuncAdd A).(f,
  g),h)
proof
  let A be set, f,g,h be Element of Funcs(A,REAL);
  thus (RealFuncAdd A).(f,(RealFuncAdd A).(g,h))
     = (RealFuncAdd A).(f,addreal.:(g,h)) by Def1
    .= addreal.:(f,addreal.:(g,h)) by Def1
    .= addreal.:(addreal.:(f,g),h) by FUNCOP_1:61
    .= (RealFuncAdd A).(addreal.:(f,g),h) by Def1
    .= (RealFuncAdd A).((RealFuncAdd A).(f,g),h) by Def1;
end;

theorem Th7:
 for A be set, f,g be Element of Funcs(A,REAL) holds
  (RealFuncMult A).(f,g) = (RealFuncMult A).(g,f)
proof let A be set, f,g be Element of Funcs(A,REAL);
  thus (RealFuncMult A).(f,g) = multreal.:(f,g) by Def2
    .= multreal.:(g,f) by FUNCOP_1:65
    .= (RealFuncMult A).(g,f) by Def2;
end;

theorem Th8:
 for A be set, f,g,h be Element of Funcs(A,REAL) holds
  (RealFuncMult(A)).(f,(RealFuncMult(A)).(g,h)) = (RealFuncMult(A)
  ).((RealFuncMult(A)).(f,g),h)
proof
  let A be set, f,g,h be Element of Funcs(A,REAL);
  thus (RealFuncMult A).(f,(RealFuncMult A).(g,h))
     = (RealFuncMult A).(f,multreal.:(g,h)) by Def2
    .= multreal.:(f,multreal.:(g,h)) by Def2
    .= multreal.:(multreal.:(f,g),h) by FUNCOP_1:61
    .= (RealFuncMult A).(multreal.:(f,g),h) by Def2
    .= (RealFuncMult A).((RealFuncMult A).(f,g),h) by Def2;
end;

theorem Th9:
 for A being set, f being Element of Funcs(A,REAL) holds
  (RealFuncMult(A)).(RealFuncUnit(A),f) = f
proof
  let A be set, f being Element of Funcs(A,REAL);
  per cases;
  suppose
    A = {};
    then
A1: f = {};
    thus (RealFuncMult A).(RealFuncUnit(A),f)
       = multreal.:(RealFuncUnit(A),f) by Def2
      .= f by A1;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus ((RealFuncMult A).(RealFuncUnit(A),f)).x
         = (RealFuncUnit(A)).x * f.x by Th2
        .= 1 * f.x by FUNCOP_1:7
        .= f.x;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th10:
  for A being set, f being Element of Funcs(A,REAL) holds (
  RealFuncAdd A).(RealFuncZero(A),f) = f
proof
  let A be set, f being Element of Funcs(A,REAL);
  per cases;
  suppose
    A = {};
    then
A1: f = {};
    thus (RealFuncAdd A).(RealFuncZero(A),f) = addreal.:(RealFuncZero(A),f) by
Def1
      .= f by A1;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus ((RealFuncAdd A).(RealFuncZero(A),f)).x = (RealFuncZero(A)).x + f.x
      by Th1
        .= 0 + f.x by FUNCOP_1:7
        .= f.x;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th11:
  for A being set, f be Element of Funcs(A,REAL) holds (
  RealFuncAdd A).(f,(RealFuncExtMult A).[-1,f]) = RealFuncZero(A)
proof
  let A be set, f be Element of Funcs(A,REAL);
  per cases;
  suppose
A1: A = {};
    hence (RealFuncAdd A).(f,(RealFuncExtMult A).[-1,f]) = {}
      .= RealFuncZero(A) by A1;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      set y=f.x;
      thus ((RealFuncAdd A).(f,(RealFuncExtMult A).[-1,f])).x = f.x + ((
      RealFuncExtMult A).[-1,f]).x by Th1
        .= f.x + ((-1)*y) by Th4
        .= (RealFuncZero(A)).x by FUNCOP_1:7;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th12:
  for A being set, f being Element of Funcs(A,REAL) holds (
  RealFuncExtMult A).(1,f) = f
proof
  let A be set, f be Element of Funcs(A,REAL);
  per cases;
  suppose
    A = {};
    then
A1: f = {};
    thus (RealFuncExtMult A).(1,f) = multreal[;](1,f) by Def3
      .= f by A1;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    reconsider g = (RealFuncExtMult A).(1,f) as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus g.x = 1*(f.x) by Th4
        .= f.x;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th13:
  for A being set, f being Element of Funcs(A,REAL) holds (
RealFuncExtMult A).(a,(RealFuncExtMult A).(b,f)) = (RealFuncExtMult A).(a*b,f)
proof
  let A be set, f be Element of Funcs(A,REAL);
  per cases;
  suppose
A1: A = {};
    (RealFuncExtMult A).(b,f) = multreal[;](b,f) by Def3;
    hence (RealFuncExtMult A).(a,(RealFuncExtMult A).(b,f)) = multreal[;](a,
    multreal[;](b,f)) by Def3
      .= multreal[;](a*b,f) by A1
      .= (RealFuncExtMult A).(a*b,f) by Def3;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus ((RealFuncExtMult A).[a,(RealFuncExtMult A).[b,f]]).x = a*(((
      RealFuncExtMult A).[b,f]).x) by Th4
        .= a*(b*(f.x)) by Th4
        .= (a*b)*(f.x)
        .= ((RealFuncExtMult A).[a*b,f]).x by Th4;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th14:
  for A being set, f being Element of Funcs(A,REAL) holds (
  RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(b,f)) = (
  RealFuncExtMult A).(a+b,f)
proof
  let A be set, f be Element of Funcs(A,REAL);
  per cases;
  suppose
A1: A = {};
    hence
    (RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(b,f)) = {}
      .= multreal[;](a+b,f) by A1
      .= (RealFuncExtMult A).(a+b,f) by Def3;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b
,f])).x = ((RealFuncExtMult A).[a,f]).x + ((RealFuncExtMult A).[b,f]).x by Th1
        .= a*(f.x) + ((RealFuncExtMult A).[b,f]).x by Th4
        .= a*(f.x) + b*(f.x) by Th4
        .= (a+b)*(f.x)
        .= ((RealFuncExtMult A).[a+b,f]).x by Th4;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

Lm2: for A being set, f,g being Element of Funcs(A,REAL) holds (RealFuncAdd A)
. ((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(a,g)) = (RealFuncExtMult A).(
a,(RealFuncAdd A).(f,g))
proof
  let A be set, f,g be Element of Funcs(A,REAL);
  per cases;
  suppose
A1: A = {};
    hence
    (RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(a,g)) = {}
      .= multreal[;](a,(RealFuncAdd A).(f,g)) by A1
      .= (RealFuncExtMult A).(a,(RealFuncAdd A).(f,g)) by Def3;
  end;
  suppose
    A <> {};
    then reconsider A as non empty set;
    reconsider f,g as Element of Funcs(A,REAL);
    now
      let x be Element of A;
      thus ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[a
,g])).x = ((RealFuncExtMult A).[a,f]).x + ((RealFuncExtMult A).[a,g]).x by Th1
        .= a*(f.x) + ((RealFuncExtMult A).[a,g]).x by Th4
        .= a*(f.x) + a*(g.x) by Th4
        .= a*(f.x + g.x)
        .= a*(((RealFuncAdd A).(f,g)).x) by Th1
        .= ((RealFuncExtMult A).[a,(RealFuncAdd A).(f,g)]).x by Th4;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th15:
 for A be set, f,g,h be Element of Funcs(A,REAL) holds
  (RealFuncMult(A)).(f,(RealFuncAdd A).(g,h)) = (RealFuncAdd A).((
  RealFuncMult(A)).(f,g),(RealFuncMult(A)).(f,h))
proof
  let A be set, f,g,h be Element of Funcs(A,REAL);
A1: multreal.:(f,addreal.:(g,h)) = addreal.:(multreal.:(f,g),multreal.:(f,h))
   proof let a be Element of A;
    per cases;
    suppose A = {};
    then
 f = {};
    hence (multreal.:(f,addreal.:(g,h))).a
       = (addreal.:(multreal.:(f,g),multreal.:(f,h))).a;
    end;
    suppose
      A <> {};
      then reconsider B=A as non empty set;
      reconsider ff=f, gg=g, hh=h as Element of Funcs(B,REAL);
      reconsider b = a as Element of B;
     thus (multreal.:(f,addreal.:(g,h))).a
        = multreal.(f.b,addreal.:(g,h).b) by FUNCOP_1:37
       .= multreal.(f.b,addreal.(g.b,h.b)) by FUNCOP_1:37
       .= ff.b * addreal.(gg.b,hh.b) by BINOP_2:def 11
       .= ff.b * (gg.b + hh.b) by BINOP_2:def 9
       .= (ff.b * gg.b) + (ff.b * hh.b)
       .= (ff.b * gg.b) + multreal.(ff.b,hh.b) by BINOP_2:def 11
       .= multreal.(ff.b,gg.b) + multreal.(ff.b,hh.b) by BINOP_2:def 11
       .= addreal.(multreal.(f.a,g.a),multreal.(f.a,h.a)) by BINOP_2:def 9
       .= addreal.(multreal.(f.a,g.a),multreal.:(ff,h).a) by FUNCOP_1:37
       .= addreal.(multreal.:(ff,g).a,multreal.:(ff,h).a) by FUNCOP_1:37
       .= (addreal.:(multreal.:(f,g),multreal.:(f,h))).a by FUNCOP_1:37;
    end;
   end;
  thus (RealFuncMult(A)).(f,(RealFuncAdd A).(g,h))
    = (RealFuncMult(A)).(f,addreal.:(g,h)) by Def1
   .= multreal.:(f,addreal.:(g,h)) by Def2
   .= addreal.:(multreal.:(f,g),multreal.:(f,h)) by A1
   .= (RealFuncAdd A).(multreal.:(f,g),multreal.:(f,h)) by Def1
   .= (RealFuncAdd A).((RealFuncMult(A)).(f,g),multreal.:(f,h)) by Def2
   .= (RealFuncAdd A).((RealFuncMult A).(f,g),(RealFuncMult A).(f,h)) by Def2;
end;

theorem Th16:
 for A being set, f,g,h be Element of Funcs(A,REAL), a being Real holds
  (RealFuncMult A).((RealFuncExtMult A).(a,f),g)
   = (RealFuncExtMult A).(a,(RealFuncMult A).(f,g))
proof
  let A be set, f,g,h be Element of Funcs(A,REAL), a be Real;
 thus (RealFuncMult A).((RealFuncExtMult A).(a,f),g)
   = (RealFuncMult A).(multreal[;](a,f),g) by Def3
  .= multreal.:(multreal[;](a,f),g) by Def2
  .= multreal[;](a,multreal.:(f,g)) by FUNCOP_1:85
  .= (RealFuncExtMult A).(a,multreal.:(f,g)) by Def3
  .= (RealFuncExtMult A).(a,(RealFuncMult A).(f,g)) by Def2;
end;

theorem Th17:
  ex f,g st (for z st z in A holds (z=x1 implies f.z = 1) & (z<>x1
  implies f.z = 0)) & for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1
  implies g.z = 1)
proof
  deffunc G(set) = 1;
  deffunc F(set) = 0;
  defpred P[set] means $1 = x1;
A1: for z st z in A holds (P[z] implies G(z) in REAL) & (not P[z] implies F(
  z) in REAL);
  consider f being Function of A,REAL such that
A2: for z 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 st z in A holds (P[z] implies F(z) in REAL) & (not P[z] implies G(
  z) in REAL);
  consider g being Function of A,REAL such that
A4: for z 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,REAL) 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 = 1) & (z<>x1 implies f.z = 0)) & (for z st z in A holds (z=x1
implies g.z = 0) & (z<>x1 implies g.z = 1)) implies for a,b st (RealFuncAdd A).
((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]) = RealFuncZero(A) holds a
  =0 & b=0
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 = 1) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1);
A5: f.x2=0 & g.x2=1 by A2,A3,A4;
A6: f.x1=1 & g.x1=0 by A1,A4;
  let a,b;
  reconsider x1,x2 as Element of A by A1,A2;
  assume
A7: (RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,
  g]) = RealFuncZero(A);
  then
A8: 0 = ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b
  ,g])).x2 by FUNCOP_1:7
    .= (((RealFuncExtMult A).[a,f]).x2) + (((RealFuncExtMult A).[b,g]).x2)
  by Th1
    .= a*(f.x2) + (((RealFuncExtMult A).[b,g]).x2) by Th4
    .=0 + b*1 by A5,Th4
    .= b;
  0 = ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b
  ,g])).x1 by A7,FUNCOP_1:7
    .= (((RealFuncExtMult A).[a,f]).x1) + (((RealFuncExtMult A).[b,g]).x1)
  by Th1
    .= a*(f.x1) + (((RealFuncExtMult A).[b,g]).x1) by Th4
    .= a + b*0 by A6,Th4
    .= a;
  hence thesis by A8;
end;

theorem
  x1 in A & x2 in A & x1<>x2 implies ex f,g st for a,b st (RealFuncAdd A
  ). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]) = RealFuncZero(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 = 1) & (z<>x1 implies f.z
  = 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1)
  by Th17;
  take f,g;
  let a,b;
  assume (RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g
  ]) = RealFuncZero(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
= 1) & (z<>x1 implies f.z = 0)) & (for z st z in A holds (z=x1 implies g.z = 0)
& (z<>x1 implies g.z = 1)) implies for h holds ex a,b st h = (RealFuncAdd A). (
  (RealFuncExtMult A).[a,f],(RealFuncExtMult 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 = 1) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1);
  x2 in A by A1,TARSKI:def 2;
  then
A4: f.x2=0 & g.x2=1 by A2,A3;
  x1 in A by A1,TARSKI:def 2;
  then
A5: f.x1=1 & g.x1=0 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: ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g
])).x2 = (((RealFuncExtMult A).[a,f]).x2) + (((RealFuncExtMult A).[b,g]).x2)
by Th1
      .= a*(f.x2) + (((RealFuncExtMult A).[b,g]).x2) by Th4
      .= 0 + b*1 by A4,Th4
      .= h.x2;
    ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g
])).x1 = (((RealFuncExtMult A).[a,f]).x1) + (((RealFuncExtMult A).[b,g]).x1)
by Th1
      .= a*(f.x1) + (((RealFuncExtMult A).[b,g]).x1) by Th4
      .= a + b*0 by A5,Th4
      .= h.x1;
    hence
    h.x = ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult 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 = (
  RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult 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 = 1) & (z<>x1 implies f.z
=0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1)
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 (RealFuncAdd
  A).((RealFuncExtMult A).[a,f], (RealFuncExtMult A).[b,g]) = RealFuncZero(A)
holds a=0 & b=0) & for h holds ex a,b st h = (RealFuncAdd A). ((RealFuncExtMult
  A).[a,f],(RealFuncExtMult 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 = 1) & (z<>x1 implies f.z
=0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1)
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 be set;
  func RealVectSpace(A) -> strict RealLinearSpace equals
  RLSStruct(#Funcs(A,
    REAL), (RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#);
  coherence
  proof
    set S = RLSStruct(#Funcs(A,REAL), (RealFuncZero(A)),RealFuncAdd(A),
      RealFuncExtMult(A)#);
A1: S is add-associative
    proof
      let u,v,w be Element of S;
      thus thesis by Th6;
    end;
A2: S is right_complementable
    proof
      let u be Element of S;
      reconsider u9 = u as Element of Funcs(A,REAL);
      reconsider w = (RealFuncExtMult A).[-1,u9] as VECTOR of S;
      take w;
      thus thesis by Th11;
    end;
A3: S is vector-distributive scalar-distributive scalar-associative
     scalar-unital
    proof
      thus for a being real number for v,w being Element of S holds a * (v + w
      ) = a * v + a * w
      proof
        let a be real number;
        reconsider a as Real by XREAL_0:def 1;
        for v,w being Element of S holds a * (v + w) = a * v + a * w by Lm2;
        hence thesis;
      end;
      thus for a,b being real number for v being Element of S holds (a + b) *
      v = a * v + b * v
      proof
        let a,b be real number;
        reconsider a,b as Real by XREAL_0:def 1;
        for v being Element of S holds (a + b) * v = a * v + b * v by Th14;
        hence thesis;
      end;
      thus for a,b being real number for v being Element of S holds (a * b) *
      v = a * (b * v)
      proof
        let a,b be real number;
        reconsider a,b as Real by XREAL_0:def 1;
        for v being Element of S holds (a * b) * v = a * (b * v) by Th13;
        hence thesis;
      end;
      let v being Element of S;
      thus 1 * v = v by Th12;
    end;
A4: S is right_zeroed
    proof
      let u be Element of S;
      reconsider u9=u as Element of Funcs(A,REAL);
      thus u+0.S = (RealFuncAdd A).(RealFuncZero(A),u9) by Th5
        .= u by Th10;
    end;
    S is Abelian
    proof
      let u,v be Element of S;
      thus thesis by Th5;
    end;
    hence thesis by A1,A4,A2,A3;
  end;
end;

theorem
  ex V being strict RealLinearSpace st ex u,v being Element of V st (for
a,b st a*u + b*v = 0.V holds a=0 & b=0) & for w being Element of V ex a,b st w
  = a*u + b*v
proof
  set A ={0,1};
  take V = RealVectSpace(A);
  consider f,g being Element of Funcs(A,REAL) such that
A1: for a,b st (RealFuncAdd A).((RealFuncExtMult A).[a,f], (
  RealFuncExtMult A).[b,g]) = RealFuncZero(A) holds a=0 & b=0 and
A2: for h being Element of Funcs(A,REAL) holds ex a,b st h = (
RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]) by Th22;
  reconsider u=f, v=g as Element of V;
  take u,v;
  thus for a,b st a*u + b*v = 0.V holds a=0 & b=0 by A1;
  thus for w being Element of V ex a,b st w = a*u + b*v
  proof
    let w be Element of V;
    reconsider h=w as Element of Funcs(A,REAL);
    consider a,b such that
A3: h = (RealFuncAdd A).((RealFuncExtMult A).[a,f], (RealFuncExtMult A
    ).[b,g]) by A2;
    h = a*u + b*v by A3;
    hence thesis;
  end;
end;

definition
  let A;

  func RRing(A) -> strict doubleLoopStr equals
  doubleLoopStr(#Funcs(A,REAL),
    RealFuncAdd A,RealFuncMult A, RealFuncUnit A,RealFuncZero A#);
  correctness;
end;

registration
  let A;
  cluster RRing A -> non empty;
  coherence;
end;

Lm3: now
  let A;
  set FR = RRing(A);
  let h, a be Element of FR;
  reconsider g = h as Element of Funcs(A,REAL);
  assume
A1: a = RealFuncUnit(A);
  hence h * a = (RealFuncMult(A)).(RealFuncUnit(A),g) by Th7
    .= h by Th9;
  thus a * h = h by A1,Th9;
end;

registration
  let A;
  cluster RRing(A) -> unital;
  coherence
  proof
    reconsider e = RealFuncUnit(A) as Element of RRing(A);
    take e;
    thus thesis by Lm3;
  end;
end;

theorem
  1.RRing(A) = RealFuncUnit(A);

theorem Th25:
  for x,y,z being Element of RRing(A) holds x+y = y+x & (x+y)+z =
x+(y+z) & x+(0.RRing(A)) = x & (ex t being Element of RRing(A) st x+t=(0.RRing(
A))) & x*y = y*x & (x*y)*z = x*(y*z) & x*(1.RRing(A)) = x & (1.RRing(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 RRing(A);
  set IT = RRing(A);
  reconsider f=x as Element of Funcs(A,REAL);
  thus x+y = y+x by Th5;
  thus (x+y)+z = x+(y+z) by Th6;
  thus x+(0.RRing(A)) = (RealFuncAdd A).(RealFuncZero(A),f) by Th5
    .= x by Th10;
  thus ex t being Element of RRing(A) st x+t=(0.RRing(A))
  proof
    set h = (RealFuncExtMult A).[-1,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.RRing(A)) = (RealFuncMult(A)).(RealFuncUnit(A),f) by Th7
    .= x by Th9;
  hence (1.RRing(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;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
    associative commutative right_unital right-distributive for 1-element
    doubleLoopStr;
  existence
  proof
    take L = Trivial-doubleLoopStr;
    thus L is strict;
    thus L is Abelian
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is add-associative
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is right_zeroed
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is right_complementable
    proof
      let x be Element of L;
      take x;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is associative
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is commutative
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is right_unital
    proof
      let x be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    let x be Element of L;
    thus thesis by STRUCT_0:def 10;
  end;
end;

definition
  mode Ring is Abelian add-associative right_zeroed right_complementable
    associative well-unital distributive non empty doubleLoopStr;
end;

theorem
  RRing(A) is commutative Ring
proof
A1: RRing A is Abelian
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
A2: RRing A is add-associative
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
A3: RRing A is right_complementable
  proof
    let x be Element of RRing A;
    consider t being Element of RRing A such that
A4: x+t = 0.RRing(A) by Th25;
    take t;
    thus thesis by A4;
  end;
A5: RRing A is right_zeroed
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
A6: RRing A is distributive
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
A7: RRing A is well-unital
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
A8: RRing A is associative
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
  RRing A is commutative
  proof
    let x be Element of RRing A;
    thus thesis by Th25;
  end;
  hence thesis by A1,A2,A5,A3,A8,A7,A6;
end;

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

registration
  cluster non empty for AlgebraStr;
  existence
  proof

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

definition
  let A be set;

  func RAlgebra A -> strict AlgebraStr equals
  AlgebraStr(#Funcs(A,REAL),
    RealFuncMult(A),RealFuncAdd(A), RealFuncExtMult(A),(RealFuncUnit(A)),(
    RealFuncZero(A))#);
  correctness;
end;

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

Lm4: now
  let A;
  set F = RAlgebra(A);
  let x, e be Element of F;
  reconsider f = x as Element of Funcs(A,REAL);
  assume
A1: e = RealFuncUnit(A);
  hence x * e = (RealFuncMult(A)).(RealFuncUnit(A),f) by Th7
    .= x by Th9;
  thus e * x = x by A1,Th9;
end;

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

theorem
  1.RAlgebra(A) = RealFuncUnit(A);

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

registration let A be set;
 cluster RAlgebra A -> non empty;
 coherence;
end;

registration let A be set;
 cluster RAlgebra A -> strict Abelian add-associative right_zeroed
    right_complementable commutative associative right_unital
    right-distributive vector-associative scalar-associative
    vector-distributive scalar-distributive;
 coherence
  proof
   thus RAlgebra A is strict;
   thus RAlgebra A is Abelian proof let x,y be Element of RAlgebra A;
     thus x+y = y+x by Th5;
    end;
   thus RAlgebra A is add-associative proof let x,y,z be Element of RAlgebra A;
     thus x+y+z = x+(y+z) by Th6;
    end;
   thus RAlgebra A is right_zeroed proof let x be Element of RAlgebra A;
     thus x+0.RAlgebra A = (RealFuncAdd A).(RealFuncZero A,x) by Th5
         .= x by Th10;
    end;
   thus RAlgebra A is right_complementable
    proof
      let x be Element of RAlgebra A;
      reconsider f=x as Element of Funcs(A,REAL);
      reconsider t=(RealFuncExtMult A).[-1,f] as Element of RAlgebra A;
      take t;
      thus thesis by Th11;
    end;
   thus RAlgebra A is commutative proof let x,y be Element of RAlgebra A;
     thus x*y = y*x by Th7;
    end;
   thus RAlgebra A is associative proof let x,y,z be Element of RAlgebra A;
     thus x*y*z = x*(y*z) by Th8;
    end;
   thus RAlgebra A is right_unital proof let x be Element of RAlgebra A;
     thus x*(1.RAlgebra A) = (RealFuncMult A).(RealFuncUnit A,x) by Th7
       .= x by Th9;
    end;
   thus RAlgebra A is right-distributive
    proof let x,y,z be Element of RAlgebra A;
     thus x*(y+z) = x*y + x*z by Th15;
    end;
   thus RAlgebra A is vector-associative
    proof let x,y be Element of RAlgebra A; let a;
     thus (a*x)*y = a*(x*y) by Th16;
    end;
   thus RAlgebra A is scalar-associative
    proof let a,b be real number; let x be Element of RAlgebra A;
      reconsider a,b as Element of REAL by XREAL_0:def 1;
      (a*b)*x = a*(b*x) by Th13;
     hence thesis;
    end;
   thus RAlgebra A is vector-distributive
    proof let a be real number, v,w being Element of RAlgebra A;
      reconsider a as Element of REAL by XREAL_0:def 1;
      a * (v + w) = a * v + a * w by Lm2;
     hence thesis;
    end;
   let a,b be real number, v being Element of RAlgebra A;
    reconsider a,b as Element of REAL by XREAL_0:def 1;
    (a + b) * v = a * v + b * v by Th14;
   hence thesis;
  end;
end;

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

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