The Mizar article:

Properties of Fields

by
Jozef Bialas

Received June 20, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: REALSET2
[ MML identifier index ]


environ

 vocabulary BOOLE, REALSET1, FUNCT_1, RELAT_1, BINOP_1, RLVECT_1, QC_LANG1,
      VECTSP_1, REALSET2;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      FUNCT_2, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, REALSET1;
 constructors ENUMSET1, REALSET1, MEMBERED, XBOOLE_0;
 clusters REALSET1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, ENUMSET1, REALSET1, RELAT_1,
      VECTSP_1, RELSET_1, XBOOLE_0;
 schemes FUNCT_2;

begin

:: Properties of fields

     consider x,y being set such that
Lm1:  x<>y by VECTSP_1:78;
     set Z = {x,y};
Lm2:  x in Z by TARSKI:def 2;
Lm3:  y in Z by TARSKI:def 2;
       for s being Element of Z holds Z\{s} is non empty set
     proof
         let s be Element of Z;
         per cases by TARSKI:def 2;
         suppose
       s=x;
         then not y in {s} by Lm1,TARSKI:def 1;
         hence thesis by Lm3,XBOOLE_0:def 4;
         suppose
          s=y;
         then not x in {s} by Lm1,TARSKI:def 1;
         hence thesis by Lm2,XBOOLE_0:def 4;
     end;
     then reconsider A = Z as non trivial set by REALSET1:34;
     reconsider nd = x as Element of A by TARSKI:def 2;
Lm4:  for t being set holds t in [:A,A:] iff
     (t=[x,x] or t=[x,y] or t=[y,x] or t=[y,y])
     proof
        let t be set;
          t in [:A,A:] implies (t=[x,x] or t=[x,y] or t=[y,x] or t=[y,y])
        proof
           assume t in [:A,A:];
           then consider t1,t2 being set such that
        A1:t1 in A & t2 in A & t=[t1,t2] by ZFMISC_1:def 2;
          (t1=x or t1=y) & (t2=x or t2=y) by A1,TARSKI:def 2;
           hence thesis by A1;
        end;
        hence thesis by Lm2,Lm3,ZFMISC_1:def 2;
     end;
       for t being set holds t in [:A,A:] iff t in {[x,x],[x,y],[y,x],[y,y]}
     proof
         let t be set;
           t in {[x,x],[x,y],[y,x],[y,y]} iff
         (t=[x,x] or t=[x,y] or t=[y,x] or t=[y,y]) by ENUMSET1:18,19;
         hence thesis by Lm4;
     end;
then Lm5: [:A,A:] = {[x,x],[x,y],[y,x],[y,y]} by TARSKI:2;
     set x1=[[x,x],x], x2=[[x,y],y], x3=[[y,x],y], x4=[[y,y],x];
     set F={x1,x2,x3,x4};
Lm6: for p being set st p in F ex q,r being set st [q,r] = p
     proof
         let p be set;
         assume p in F;
         then p=[[x,x],x] or p=[[x,y],y] or p=[[y,x],y] or p=[[y,y],x]
           by ENUMSET1:18;
         hence thesis;
     end;
       for q,r1,r2 being set st [q,r1] in F & [q,r2] in F holds r1 = r2
     proof
         let q,r1,r2 be set;
         assume
      A1:[q,r1] in F & [q,r2] in F;
         then A2:[q,r1]=[[x,x],x] or [q,r1]=[[x,y],y] or
         [q,r1]=[[y,x],y] or [q,r1]=[[y,y],x] by ENUMSET1:18;
           [q,r2]=[[x,x],x] or [q,r2]=[[x,y],y] or
         [q,r2]=[[y,x],y] or [q,r2]=[[y,y],x] by A1,ENUMSET1:18;
         then ((q=[x,x] & r1=x) or (q=[x,y] & r1=y) or
         (q=[y,x] & r1=y) or (q=[y,y] & r1=x)) &
         ((q=[x,x] & r2=x) or (q=[x,y] & r2=y) or
         (q=[y,x] & r2=y) or (q=[y,y] & r2=x)) by A2,ZFMISC_1:33;
         hence thesis by ZFMISC_1:33;
     end;
     then reconsider od = F as Function by Lm6,FUNCT_1:2;
       for t being set holds t in [:A,A:] iff ex r being set st [t,r] in F
     proof
         let t be set;
      A1:t in [:A,A:] implies ex r being set st [t,r] in F
         proof
             assume
A2:          t in [:A,A:];
         A3:(t=[x,x] or t=[y,y]) implies ex r being set st [t,r] in F
             proof
                 assume t=[x,x] or t=[y,y];
                 then [t,x] in F by ENUMSET1:19;
                 hence thesis;
             end;
               (t=[x,y] or t=[y,x]) implies ex r being set st [t,r] in F
             proof
                 assume t=[x,y] or t=[y,x];
                 then [t,y] in F by ENUMSET1:19;
                 hence thesis;
             end;
             hence thesis by A2,A3,Lm5,ENUMSET1:18;
         end;
           (ex r being set st [t,r] in F) implies t in [:A,A:]
         proof
            given r being set such that
         A4:[t,r] in F;
              [t,r]=[[x,x],x] or [t,r]=[[x,y],y] or
            [t,r]=[[y,x],y] or [t,r]=[[y,y],x] by A4,ENUMSET1:18;
            then t=[x,x] or t=[x,y] or t=[y,x] or t=[y,y] by ZFMISC_1:33;
            hence thesis by Lm4;
         end;
         hence thesis by A1;
     end;
then Lm7:[:A,A:] = dom od by RELAT_1:def 4;
 then Lm8: [x,x] in dom od by Lm4;
     Lm9: [[x,x],x] in od by ENUMSET1:19;
then Lm10: od.[x,x]=x by Lm8,FUNCT_1:def 4;
 Lm11: [x,y] in dom od by Lm4,Lm7;
     Lm12: [[x,y],y] in od by ENUMSET1:19;
then Lm13:od.[x,y]=y by Lm11,FUNCT_1:def 4;
 Lm14: [y,x] in dom od by Lm4,Lm7;
     Lm15: [[y,x],y] in od by ENUMSET1:19;
then Lm16:od.[y,x]=y by Lm14,FUNCT_1:def 4;
 Lm17: [y,y] in dom od by Lm4,Lm7;
       [[y,y],x] in od by ENUMSET1:19;
then Lm18:od.[y,y]=x by Lm17,FUNCT_1:def 4;
then Lm19:for t being set st t in [:A,A:] holds od.t in A
     by Lm2,Lm3,Lm4,Lm10,Lm13,Lm16;
     set s2=[[x,y],x], s3=[[y,x],x], s4=[[y,y],y];
     set D={x1,s2,s3,s4};
Lm20:for p being set st p in D ex q,r being set st [q,r] = p
     proof
         let p be set;
         assume p in D;
         then p=[[x,x],x] or p=[[x,y],x] or p=[[y,x],x] or p=[[y,y],y]
         by ENUMSET1:18;
         hence thesis;
     end;
       for q,r1,r2 being set st [q,r1] in D & [q,r2] in D holds r1 = r2
     proof
         let q,r1,r2 be set;
         assume
      A1:[q,r1] in D & [q,r2] in D;
      then A2:[q,r1]=[[x,x],x] or [q,r1]=[[x,y],x] or
         [q,r1]=[[y,x],x] or [q,r1]=[[y,y],y] by ENUMSET1:18;
           [q,r2]=[[x,x],x] or [q,r2]=[[x,y],x] or
         [q,r2]=[[y,x],x] or [q,r2]=[[y,y],y] by A1,ENUMSET1:18;
         then ((q=[x,x] & r1=x) or (q=[x,y] & r1=x) or
         (q=[y,x] & r1=x) or (q=[y,y] & r1=y)) &
         ((q=[x,x] & r2=x) or (q=[x,y] & r2=x) or
         (q=[y,x] & r2=x) or (q=[y,y] & r2=y)) by A2,ZFMISC_1:33;
         hence thesis by ZFMISC_1:33;
     end;
     then reconsider om = D as Function by Lm20,FUNCT_1:2;
       for t being set holds t in [:A,A:] iff ex r being set st [t,r] in D
     proof
         let t be set;
     A1:t in [:A,A:] implies ex r being set st [t,r] in D
         proof
           assume
A2:        t in [:A,A:];
        A3:(t=[x,x] or t=[x,y] or t=[y,x]) implies
           ex r being set st [t,r] in D
             proof
                 assume t=[x,x] or t=[x,y] or t=[y,x];
                 then [t,x] in D by ENUMSET1:19;
                 hence thesis;
             end;
               t=[y,y] implies ex r being set st [t,r] in D
             proof
                 assume t=[y,y];
                 then [t,y] in D by ENUMSET1:19;
                 hence thesis;
             end;
             hence thesis by A2,A3,Lm5,ENUMSET1:18;
         end;
           (ex r being set st [t,r] in D) implies t in [:A,A:]
         proof
            given r being set such that
         A4:[t,r] in D;
              [t,r]=[[x,x],x] or [t,r]=[[x,y],x] or
            [t,r]=[[y,x],x] or [t,r]=[[y,y],y] by A4,ENUMSET1:18;
            then t=[x,x] or t=[x,y] or t=[y,x] or t=[y,y] by ZFMISC_1:33;
            hence thesis by Lm4;
         end;
         hence thesis by A1;
     end;
then Lm21: [:A,A:] = dom om by RELAT_1:def 4;
 then Lm22: [x,x] in dom om by Lm4;
       [[x,x],x] in om by ENUMSET1:19;
then Lm23:om.[x,x]=x by Lm22,FUNCT_1:def 4;
 Lm24: [x,y] in dom om by Lm4,Lm21;
       [[x,y],x] in om by ENUMSET1:19;
then Lm25: om.[x,y]=x by Lm24,FUNCT_1:def 4;
 Lm26: [y,x] in dom om by Lm4,Lm21;
       [[y,x],x] in om by ENUMSET1:19;
then Lm27:om.[y,x]=x by Lm26,FUNCT_1:def 4;
 Lm28: [y,y] in dom om by Lm4,Lm21;
       [[y,y],y] in om by ENUMSET1:19;
then Lm29:om.[y,y]=y by Lm28,FUNCT_1:def 4;
then Lm30:for t being set st t in [:A,A:] holds om.t in A
         by Lm2,Lm3,Lm4,Lm23,Lm25,Lm27;
then Lm31:om is BinOp of A by Lm21,FUNCT_2:5;
Lm32:A\{x}={y} by Lm1,ZFMISC_1:23;
  then Lm33:[:A\{x},A\{x}:] = {[y,y]} by ZFMISC_1:35;
Lm34: for t being set holds t in [:A\{x},A\{x}:] implies om.t in A\{x}
     proof
        let t be set;
        assume t in [:A\{x},A\{x}:];
        then t=[y,y] by Lm33,TARSKI:def 1;
        hence thesis by Lm29,Lm32,TARSKI:def 1;
     end;
     reconsider nm = y as Element of A\{nd} by Lm32,TARSKI:def 1;
     reconsider od0=od as BinOp of A by Lm7,Lm19,FUNCT_2:5;
     reconsider om0=om as BinOp of A by Lm21,Lm30,FUNCT_2:5;
Lm35: for a,b,d being Element of A holds
     od0.[od0.[a,b],d] = od0.[a,od0.[b,d]]
     proof
       let a,b,d be Element of A;
         (a=x & b=x & d=x) or (a=x & b=x & d=y) or (a=x & b=y & d=x) or
       (a=x & b=y & d=y) or (a=y & b=x & d=x) or (a=y & b=x & d=y) or
       (a=y & b=y & d=x) or (a=y & b=y & d=y) by TARSKI:def 2;
       hence thesis by Lm10,Lm13,Lm16,Lm18;
     end;
Lm36: for a being Element of A holds od0.[a,nd] = a & od0.[nd,a] = a
     proof
       let a be Element of A;
         a=x or a=y by TARSKI:def 2;
       hence thesis by Lm8,Lm9,Lm11,Lm12,Lm14,Lm15,FUNCT_1:def 4;
     end;
Lm37: for a being Element of A ex b being Element of A st
     od0.[a,b] = nd & od0.[b,a] = nd
     proof
       let a be Element of A;
         a=x or a=y by TARSKI:def 2;
       hence thesis by Lm10,Lm18;
     end;
       for a,b being Element of A holds od0.[a,b] = od0.[b,a]
     proof
       let a,b be Element of A;
         (a=x & b=x) or (a=x & b=y) or (a=y & b=x) or (a=y & b=y)
         by TARSKI:def 2;
       hence thesis by Lm11,Lm12,Lm16,FUNCT_1:def 4;
     end;
then Lm38: LoopStr(#A,od0,nd#) is Group
      by Lm35,Lm36,Lm37,REALSET1:def 5,def 6,def 7,def 8;
     reconsider om1=om as DnT of nd,A by Lm31,Lm34,REALSET1:def 18;
Lm39:for B being non empty set, P being BinOp of B,
         e being Element of B st
     B = A\{nd} & e = nm & P = om1!(A,nd) holds LoopStr(#B,P,e#) is Group
     proof
        let B be non empty set,
            P be BinOp of B,
            e be Element of B;
        assume
    A1: B = A\{nd} & e = nm & P = om1!(A,nd);
    A2: dom P = [:B,B:] & rng P c= B by FUNCT_2:def 1,RELSET_1:12;
          [y,y] in [:B,B:] by A1,ZFMISC_1:def 2;
        then A3: P.[y,y] in rng P by A2,FUNCT_1:def 5;
    then A4: P.[y,y] = y by A1,A2,Lm32,TARSKI:def 1;
    A5: for a,b,c being Element of B holds P.[P.[a,b],c] = P.[a,P.[b,c]]
        proof
          let a,b,c be Element of B;
            a = y & b = y & c = y by A1,Lm32,TARSKI:def 1;
          hence thesis by A4;
        end;
    A6: for a being Element of B holds P.[a,e] = a & P.[e,a] = a
        proof
          let a be Element of B;
            a = y by A1,Lm32,TARSKI:def 1;
          hence thesis by A1,A2,A3,Lm32,TARSKI:def 1;
        end;
    A7: for a being Element of B ex b being Element of B st
        P.[a,b] = e & P.[b,a] = e
        proof
          let a be Element of B;
          take e;
          thus thesis by A1,A4,Lm32,TARSKI:def 1;
        end;
          for a,b being Element of B holds P.[a,b] = P.[b,a]
        proof
          let a,b be Element of B;
            a = y & b = y by A1,Lm32,TARSKI:def 1;
          hence thesis;
        end;
        hence thesis by A5,A6,A7,REALSET1:def 5,def 6,def 7,def 8;
     end;
Lm40: for a,b,d being Element of A holds
         (om0.[a,od0.[b,d]] = od0.[om0.[a,b],om0.[a,d]] &
          om0.[od0.[a,b],d] = od0.[om0.[a,d],om0.[b,d]])
     proof
       let a,b,d be Element of A;
         (a=x & b=x & d=x) or (a=x & b=x & d=y) or
       (a=x & b=y & d=x) or (a=x & b=y & d=y) or
       (a=y & b=x & d=x) or (a=y & b=x & d=y) or
       (a=y & b=y & d=x) or (a=y & b=y & d=y) by TARSKI:def 2;
       hence thesis by Lm10,Lm13,Lm16,Lm18,Lm23,Lm25,Lm27,Lm29;
     end;

definition
  let IT be doubleLoopStr;
  attr IT is Field-like means
:Def1:   ex A being non trivial set,
            od being BinOp of A, nd being Element of A,
            om being DnT of nd,A, nm being Element of A\{nd} st
           (IT = field(A,od,om,nd,nm) & LoopStr(#A,od,nd#) is Group &
           (for B being non empty set, P being BinOp of B,
                e being Element of B holds
               (B = A\{nd} & e = nm & P = om!(A,nd) implies
           LoopStr(#B,P,e#) is Group)) &
           for x,y,z being Element of A holds
            om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
            om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]);
end;

definition
 cluster strict Field-like doubleLoopStr;
  existence
   proof
      field(A,od0,om0,nd,nm) is Field-like by Def1,Lm38,Lm39,Lm40;
    hence thesis;
   end;
end;

definition ::field
  mode Field is Field-like doubleLoopStr;
end;

definition ::supp projection
   let F be Field;
   func suppf(F) -> non trivial set means
:Def2:    ex od being BinOp of it,
             nd being Element of it,
             om being DnT of nd,it,
             nm being Element of it\{nd} st
           F = field(it,od,om,nd,nm);
existence
proof
     ex A being non trivial set st
   ex od being BinOp of A,
      nd being Element of A,
      om being DnT of nd,A,
      nm being Element of A\{nd} st
      (F = field(A,od,om,nd,nm) &
      LoopStr(#A,od,nd#) is Group &
      (for B being non empty set,
           P being BinOp of B,
           e being Element of B holds
           (B = A\{nd} & e = nm & P = om!(A,nd) implies
           LoopStr(#B,P,e#) is Group)) &
           for x,y,z being Element of A holds
           om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
           om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]) by Def1;
   then consider A being non trivial set,
                 od being BinOp of A,
                 nd being Element of A,
                 om being DnT of nd,A,
                 nm being Element of A\{nd} such that
A1: F = field(A,od,om,nd,nm);
   take A;
   take od, nd, om, nm;
   thus thesis by A1;
end;
uniqueness
proof
    let A1,A2 be non trivial set such that
A2: ex od1 being BinOp of A1,
       nd1 being Element of A1,
       om1 being DnT of nd1,A1,
       nm1 being Element of A1\{nd1} st
     F = field(A1,od1,om1,nd1,nm1) and
A3: ex od2 being BinOp of A2,
       nd2 being Element of A2,
       om2 being DnT of nd2,A2,
       nm2 being Element of A2\{nd2} st
     F = field(A2,od2,om2,nd2,nm2);
      A1 = the carrier of F by A2,REALSET1:def 14
      .= A2 by A3,REALSET1:def 14;
    hence thesis;
end;
end;

definition ::add projection
   let F be Field;
   func odf(F) -> BinOp of suppf(F) means
:Def3:     ex nd being Element of suppf(F),
              om being DnT of nd, suppf(F),
              nm being Element of suppf(F)\{nd} st
           F = field(suppf(F),it,om,nd,nm);
existence by Def2;
uniqueness
proof
    let od1,od2 be BinOp of suppf(F) such that
A1: ex nd1 being Element of suppf(F),
       om1 being DnT of nd1, suppf(F),
       nm1 being Element of suppf(F)\{nd1} st
     F = field(suppf(F),od1,om1,nd1,nm1) and
A2: ex nd2 being Element of suppf(F),
       om2 being DnT of nd2, suppf(F),
       nm2 being Element of suppf(F)\{nd2} st
     F = field(suppf(F),od2,om2,nd2,nm2);
      od1 = the add of F by A1,REALSET1:def 14
      .= od2 by A2,REALSET1:def 14;
    hence thesis;
end;
end;

definition ::nadd projection
   let F be Field;
   func ndf(F) -> Element of suppf(F) means
:Def4:    ex om being DnT of it,suppf(F),
             nm being Element of suppf(F)\{it} st
           F = field(suppf(F),odf(F),om,it,nm);
existence by Def3;
uniqueness
proof
    let nd1,nd2 be Element of suppf(F) such that
A1: ex om1 being DnT of nd1,suppf(F),
       nm1 being Element of suppf(F)\{nd1} st
           F = field(suppf(F),odf(F),om1,nd1,nm1) and
A2: ex om2 being DnT of nd2,suppf(F),
       nm2 being Element of suppf(F)\{nd2} st
           F = field(suppf(F),odf(F),om2,nd2,nm2);
      nd1 = the Zero of F by A1,REALSET1:def 14
      .= nd2 by A2,REALSET1:def 14;
    hence thesis;
end;
end;

definition ::mply projection
   let F be Field;
   func omf(F) -> DnT of ndf(F),suppf(F) means
:Def5:   ex nm being Element of suppf(F)\{ndf(F)} st
           F = field(suppf(F),odf(F),it,ndf(F),nm);
existence by Def4;
uniqueness
proof
    let om1,om2 be DnT of ndf(F),suppf(F) such that
A1: ex nm1 being Element of suppf(F)\{ndf(F)} st
           F = field(suppf(F),odf(F),om1,ndf(F),nm1) and
A2: ex nm2 being Element of suppf(F)\{ndf(F)} st
           F = field(suppf(F),odf(F),om2,ndf(F),nm2);
      om1 = the mult of F by A1,REALSET1:def 14
      .= om2 by A2,REALSET1:def 14;
    hence thesis;
end;
end;

definition ::nom projection
   let F be Field;
   func nmf(F) -> Element of suppf(F)\{ndf(F)} means
:Def6:       F = field(suppf(F),odf(F),omf(F),ndf(F),it);
existence by Def5;
uniqueness
proof
    let nm1,nm2 be Element of suppf(F)\{ndf(F)} such that
A1: F = field(suppf(F),odf(F),omf(F),ndf(F),nm1) and
A2: F = field(suppf(F),odf(F),omf(F),ndf(F),nm2);
      nm1 = (the unity of F) by A1,REALSET1:def 14
       .= nm2 by A2,REALSET1:def 14;
    hence thesis;
end;
end;

canceled 7;

theorem Th8:
   for F being Field holds LoopStr(#suppf(F),odf(F),ndf(F)#) is Group
proof
   let F be Field;
     ex A being non trivial set st
   ex od being BinOp of A, nd being Element of A,
   om being DnT of nd,A, nm being Element of A\{nd} st
     (F = field(A,od,om,nd,nm) & LoopStr(#A,od,nd#) is Group &
                (for B being non empty set,
                     P being BinOp of B,
                     e being Element of B holds
                (B = A\{nd} & e = nm & P = om!(A,nd) implies
                     LoopStr(#B,P,e#) is Group)) &
                for x,y,z being Element of A holds
                 om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
                 om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]) by Def1;
   then consider A being non trivial set,
                 od being BinOp of A,
                 nd being Element of A,
                 om being DnT of nd,A,
                 nm being Element of A\{nd} such that
A1:F = field(A,od,om,nd,nm) and
A2:LoopStr(#A,od,nd#) is Group;
A3:A = suppf(F) by A1,Def2;
   then od = odf(F) by A1,Def3;
   hence thesis by A1,A2,A3,Def4;
end;

theorem Th9:
   for F being Field, B being non empty set,
       P being BinOp of B, e being Element of B st
   B = suppf(F)\{ndf(F)} & e = nmf(F) & P = omf(F)!(suppf(F),ndf(F)) holds
    LoopStr(#B,P,e#) is Group
proof
   let F be Field, B be non empty set, P be BinOp of B, e be Element of B;
  ex A being non trivial set st ex od being BinOp of A,
                   nd being Element of A,
                   om being DnT of nd,A,
                   nm being Element of A\{nd} st
      (F = field(A,od,om,nd,nm) & LoopStr(#A,od,nd#) is Group &
                (for B being non empty set,
                     P being BinOp of B,
                     e being Element of B holds
                 (B = A\{nd} & e = nm & P = om!(A,nd) implies
                  LoopStr(#B,P,e#) is Group)) &
                for x,y,z being Element of A holds
                 om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
                 om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]) by Def1;
      then consider A being non trivial set,
               od being BinOp of A,
               nd being Element of A,
               om being DnT of nd,A,
               nm being Element of A\{nd} such that
A1:         F = field(A,od,om,nd,nm) and
A2:         for B being non empty set,
                P being BinOp of B,
                e being Element of B st
                B = A\{nd} & e = nm & P = om!(A,nd) holds
                  LoopStr(#B,P,e#) is Group;
A3: A = suppf(F) by A1,Def2;
   then reconsider od as BinOp of suppf(F);
   reconsider nd as Element of suppf(F) by A1,Def2;
   reconsider om as DnT of nd, suppf(F) by A1,Def2;
   reconsider nm as Element of suppf(F)\{nd} by A1,Def2;
A4:od = odf(F) by A1,A3,Def3;
A5:F = field(suppf(F),odf(F),om,nd,nm) by A1,A3,Def3;
A6:nd=ndf(F) by A1,A3,A4,Def4;
   reconsider om as DnT of ndf(F),suppf(F) by A1,A3,A4,Def4;
   reconsider nm as Element of suppf(F)\{ndf(F)} by A1,A3,A4,Def4;
A7:om=omf(F) by A5,A6,Def5;
   then A8:nm=nmf(F) by A5,A6,Def6;
   assume B = suppf(F)\{ndf(F)} & e = nmf(F) & P = omf(F)!(suppf(F),ndf(F));
   hence thesis by A2,A3,A6,A7,A8;
end;

theorem Th10:
   for F being Field, x,y,z being Element of suppf(F) holds
   (omf(F).[x,odf(F).[y,z]] = odf(F).[omf(F).[x,y],omf(F).[x,z]] &
    omf(F).[odf(F).[x,y],z] = odf(F).[omf(F).[x,z],omf(F).[y,z]] )
proof
   let F be Field;
     ex A being non trivial set,
      od being BinOp of A,
      nd being Element of A,
      om being DnT of nd, A,
      nm being Element of A\{nd} st
      (F = field(A,od,om,nd,nm) & LoopStr(#A,od,nd#) is Group &
      (for B being non empty set,
           P being BinOp of B,
           e being Element of B holds
         (B = A\{nd} & e = nm & P = om!(A,nd) implies
                     LoopStr(#B,P,e#) is Group)) &
                for x,y,z being Element of A holds
                 om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
                 om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]) by Def1;
   then consider A being non trivial set,
                 od being BinOp of A,
                 nd being Element of A,
                 om being DnT of nd,A,
                 nm being Element of A\{nd} such that
A1: F = field(A,od,om,nd,nm) and
A2:for x,y,z being Element of A holds
   (om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] &
    om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]);
A3: A = suppf(F) by A1,Def2;
   then reconsider od as BinOp of suppf(F);
   reconsider nd as Element of suppf(F) by A1,Def2;
   reconsider om as DnT of nd, suppf(F) by A1,Def2;
   reconsider nm as Element of suppf(F)\{nd} by A1,Def2;
A4:od = odf(F) by A1,A3,Def3;
A5:F = field(suppf(F),odf(F),om,nd,nm) by A1,A3,Def3;
A6:nd=ndf(F) by A1,A3,A4,Def4;
    reconsider om as DnT of ndf(F),suppf(F) by A1,A3,A4,Def4;
      om=omf(F) by A5,A6,Def5;
    hence thesis by A2,A3,A4;
end;

theorem Th11:
   for F being Field,
       a,b,c being Element of suppf(F) holds
   odf(F).[odf(F).[a,b],c] = odf(F).[a,odf(F).[b,c]]
proof
   let F be Field, a,b,c be Element of suppf(F);
     LoopStr(#suppf(F),odf(F),ndf(F)#) is Group by Th8;
   then consider D being strict Group such that
A1:D = LoopStr(#suppf(F),odf(F),ndf(F)#);
   thus thesis by A1,REALSET1:def 7;
end;

theorem Th12:
   for F being Field,
       a,b being Element of suppf(F) holds
   odf(F).[a,b] = odf(F).[b,a]
proof
   let F be Field, a,b be Element of suppf(F);
     LoopStr(#suppf(F),odf(F),ndf(F)#) is Group by Th8;
   then consider D being strict Group such that
A1:D = LoopStr(#suppf(F),odf(F),ndf(F)#);
   thus thesis by A1,REALSET1:def 8;
end;

theorem Th13:
   for F being Field,
       a being Element of suppf(F) holds
   odf(F).[a,ndf(F)] = a & odf(F).[ndf(F),a] = a
proof
   let F be Field, a be Element of suppf(F);
     LoopStr(#suppf(F),odf(F),ndf(F)#) is Group by Th8;
   then consider D being strict Group such that
A1:D = LoopStr(#suppf(F),odf(F),ndf(F)#);
   thus thesis by A1,REALSET1:def 5;
end;

theorem Th14:
   for F being Field holds
   for a being Element of suppf(F) ex b being Element of suppf(F) st
   odf(F).[a,b] = ndf(F) & odf(F).[b,a] = ndf(F)
proof
   let F be Field;
   let a be Element of suppf(F);
     LoopStr(#suppf(F),odf(F),ndf(F)#) is Group by Th8;
   then consider D being strict Group such that
A1:D = LoopStr(#suppf(F),odf(F),ndf(F)#);
   thus thesis by A1,REALSET1:def 6;
end;

definition
   let F be non trivial set;
   mode OnePoint of F -> set means
:Def7:ex x being Element of F st it = {x};
existence
proof
   consider y being Element of F;
   take {y};
   thus thesis;
end;
end;

theorem Th15:
   for F being non trivial set holds
   for A being OnePoint of F holds
   F\A is non empty set
proof
   let F be non trivial set;
   let A be OnePoint of F;
     ex x being Element of F st A = {x} by Def7;
   hence thesis by REALSET1:32;
end;

definition
   let F be non trivial set;
   let A be OnePoint of F;
   cluster F\A -> non empty;
coherence by Th15;
end;

definition
   let F be non trivial set;
 cluster non empty OnePoint of F;
 existence
  proof consider x being Element of F;
     {x} is OnePoint of F by Def7;
   hence thesis;
  end;
end;

definition
   let F be non trivial set;
   let x be Element of F;
   redefine func {x} -> OnePoint of F;
coherence by Def7;
end;

canceled 4;

theorem Th20:
   for F being Field holds
   for a,b,c being Element of suppf(F)\{ndf(F)} holds
   omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]
proof
   let F be Field;
   let a,b,c be Element of suppf(F)\{ndf(F)};
   set B = suppf(F)\{ndf(F)};
   set P = omf(F)!(suppf(F),ndf(F));
   set e = nmf(F);
   reconsider D = LoopStr(#B,P,e#) as strict Group by Th9;
   reconsider a,b,c as Element of D;
A1:omf(F)!(suppf(F),ndf(F)) =
   omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by REALSET1:def 19;
A2:omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
    is Function of [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:],
    (suppf(F)\{ndf(F)}) by REALSET1:45;
then A3:dom(omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]) =
    [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by FUNCT_2:def 1;
A4:for s,t being Element of (suppf(F)\{ndf(F)}) holds
    (the add of D).[s,t] is Element of (suppf(F)\{ndf(F)}) &
    omf(F).[s,t] is Element of (suppf(F)\{ndf(F)})
    proof
        let s,t be Element of (suppf(F)\{ndf(F)});
     A5:[s,t] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by ZFMISC_1:def 2;
        consider W being Function of
        [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:],
        (suppf(F)\{ndf(F)}) such that
    A6: W = omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by A2;
          W.[s,t] is Element of (suppf(F)\{ndf(F)}) by A5,FUNCT_2:7;
        hence thesis by A3,A5,A6,FUNCT_1:70,REALSET1:def 19;
    end;
A7:for x,y being Element of suppf(F)\{ndf(F)} holds
    omf(F).[x,y] = (the add of D).[x,y]
    proof
      let x,y be Element of suppf(F)\{ndf(F)};
        [x,y] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by ZFMISC_1:def 2;
      hence thesis by A1,A3,FUNCT_1:70;
    end;
A8:for x,y,z being Element of suppf(F)\{ndf(F)} holds
  omf(F).[(the add of D).[x,y],z] = (the add of D).[(the add of D).[x,y],z] &
    (the add of D).[x,omf(F).[y,z]] = omf(F).[x,omf(F).[y,z]]
    proof
        let x,y,z be Element of suppf(F)\{ndf(F)};
    A9:(the add of D).[x,y] is Element of suppf(F)\{ndf(F)} by A4;
          omf(F).[y,z] is Element of suppf(F)\{ndf(F)} by A4;
        hence thesis by A7,A9;
    end;
      omf(F).[omf(F).[a,b],c] = omf(F).[(the add of D).[a,b],c] by A7
                           .= (the add of D).[(the add of D).[a,b],c] by A8
                           .= (the add of D).[a,(the add of D).[b,c]]
                            by REALSET1:def 7
                           .= (the add of D).[a,omf(F).[b,c]] by A7
                           .= omf(F).[a,omf(F).[b,c]] by A8;
   hence thesis;
end;

theorem Th21:
   for F being Field holds
   for a,b being Element of suppf(F)\{ndf(F)} holds
   omf(F).[a,b] = omf(F).[b,a]
proof
   let F be Field;
   let a,b be Element of suppf(F)\{ndf(F)};
   set B = suppf(F)\{ndf(F)};
   set P = omf(F)!(suppf(F),ndf(F));
   set e = nmf(F);
   reconsider D = LoopStr(#B,P,e#) as strict Group by Th9;
   reconsider a,b as Element of D;
A1:omf(F)!(suppf(F),ndf(F)) =
   omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by REALSET1:def 19;
     omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
    is Function of [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:],
    (suppf(F)\{ndf(F)}) by REALSET1:45;
then A2: dom(omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]) =
    [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by FUNCT_2:def 1;
A3:for x,y being Element of suppf(F)\{ndf(F)} holds
    omf(F).[x,y] = (the add of D).[x,y]
    proof
        let x,y be Element of suppf(F)\{ndf(F)};
          [x,y] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by ZFMISC_1:def 2;
        hence thesis by A1,A2,FUNCT_1:70;
    end;
    then omf(F).[a,b] = (the add of D).[a,b]
                .= (the add of D).[b,a] by REALSET1:def 8
                .= omf(F).[b,a] by A3;
   hence thesis;
end;

theorem Th22:
   for F being Field holds
   for a being Element of suppf(F)\{ndf(F)} holds
   omf(F).[a,nmf(F)] = a & omf(F).[nmf(F),a] = a
proof
   let F be Field;
   let a be Element of suppf(F)\{ndf(F)};
   set B = suppf(F)\{ndf(F)};
   set P = omf(F)!(suppf(F),ndf(F));
   set e = nmf(F);
   reconsider D = LoopStr(#B,P,e#) as strict Group by Th9;
   reconsider a as Element of D;
A1:omf(F)!(suppf(F),ndf(F)) =
   omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by REALSET1:def 19;
  omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
    is Function of [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:],
    (suppf(F)\{ndf(F)}) by REALSET1:45;
then A2: dom(omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]) =
    [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by FUNCT_2:def 1;
A3:for x,y being Element of suppf(F)\{ndf(F)} holds
    omf(F).[x,y] = (the add of D).[x,y]
    proof
        let x,y be Element of suppf(F)\{ndf(F)};
      [x,y] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by ZFMISC_1:def 2;
        hence thesis by A1,A2,FUNCT_1:70;
    end;
    reconsider a as Element of suppf(F)\{ndf(F)};
A4:omf(F).[a,nmf(F)] = (the add of D).[a,the Zero of D] by A3
                     .= a by REALSET1:def 5;
     omf(F).[nmf(F),a] = (the add of D).[the Zero of D,a] by A3
                     .= a by REALSET1:def 5;
   hence thesis by A4;
end;

theorem Th23:
   for F being Field holds
   for a being Element of suppf(F)\{ndf(F)}
   ex b being Element of suppf(F)\{ndf(F)} st
   omf(F).[a,b] = nmf(F) & omf(F).[b,a] = nmf(F)
proof
   let F be Field;
   let a be Element of suppf(F)\{ndf(F)};
   set B = suppf(F)\{ndf(F)};
   set P = omf(F)!(suppf(F),ndf(F));
   set e = nmf(F);
     LoopStr(#B,P,e#) is Group by Th9;
   then consider D being strict Group such that
A1:D = LoopStr(#B,P,e#);
   reconsider a as Element of D by A1;
   consider b being Element of D such that
A2:(the add of D).[a,b] = the Zero of D & (the add of D).[b,a] = the Zero of D
    by REALSET1:def 6;
A3:omf(F)!(suppf(F),ndf(F)) =
   omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
   by REALSET1:def 19;
  omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
    is Function of [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:],
    (suppf(F)\{ndf(F)}) by REALSET1:45;
then A4: dom(omf(F)|[:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]) =
    [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by FUNCT_2:def 1;
A5:for x,y being Element of suppf(F)\{ndf(F)} holds
    omf(F).[x,y] = (the add of D).[x,y]
    proof
        let x,y be Element of suppf(F)\{ndf(F)};
      [x,y] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:]
        by ZFMISC_1:def 2;
        hence thesis by A1,A3,A4,FUNCT_1:70;
    end;
    reconsider b as Element of suppf(F)\{ndf(F)} by A1;
   take b;
   thus thesis by A1,A2,A5;
end;

definition ::complement element
   let F be Field;
   func compf(F) -> Function of suppf(F),suppf(F) means
:Def8: for x being Element of suppf(F) holds odf(F).[x,it.x] = ndf(F);
existence
proof
  defpred Z[set,set] means odf(F).[$1,$2] = ndf(F);
   A1:for x being set st x in suppf(F) ex y being set st
          y in suppf(F) & Z[x,y]
      proof
         let x be set;
         assume x in suppf(F);
         then consider y being Element of suppf(F) such that
      A2:odf(F).[x,y] = ndf(F) & odf(F).[y,x] = ndf(F) by Th14;
         take y;
         thus thesis by A2;
      end;
        ex C being Function of suppf(F),suppf(F) st
      for x being set st x in suppf(F) holds Z[x,C.x] from FuncEx1(A1);
      then consider C being Function of suppf(F),suppf(F) such that
A3:   for x being set st x in suppf(F) holds odf(F).[x,C.x] = ndf(F);
      take C;
      thus thesis by A3;
end;
uniqueness
proof
   let C1,C2 be Function of suppf(F),suppf(F) such that
A4:for x being Element of suppf(F) holds odf(F).[x,C1.x] = ndf(F) and
A5:for x being Element of suppf(F) holds odf(F).[x,C2.x] = ndf(F);
     for x being set st x in suppf(F) holds C1.x = C2.x
   proof
     let x be set;
     assume
 A6:x in suppf(F);
 then A7:C1.x is Element of suppf(F) by FUNCT_2:7;
 A8:C2.x is Element of suppf(F) by A6,FUNCT_2:7;
     thus C1.x = odf(F).[C1.x,ndf(F)] by A7,Th13
             .= odf(F).[C1.x,odf(F).[x,C2.x]] by A5,A6
             .= odf(F).[odf(F).[C1.x,x],C2.x] by A6,A7,A8,Th11
             .= odf(F).[odf(F).[x,C1.x],C2.x] by A6,A7,Th12
             .= odf(F).[ndf(F),C2.x] by A4,A6
             .= C2.x by A8,Th13;
      end;
      hence thesis by FUNCT_2:18;
end;
end;

canceled 2;

theorem Th26:
   for F being Field holds
   for x,y being Element of suppf(F) holds
   odf(F).[x,y] = ndf(F) implies y = compf(F).x
proof
   let F be Field;
   let x,y be Element of suppf(F);
   assume
A1:odf(F).[x,y] = ndf(F);
     y = odf(F).[y,ndf(F)] by Th13
         .= odf(F).[y,odf(F).[x,compf(F).x]] by Def8
         .= odf(F).[odf(F).[y,x],compf(F).x] by Th11
         .= odf(F).[ndf(F),compf(F).x] by A1,Th12
         .= compf(F).x by Th13;
   hence thesis;
end;

theorem
     for F being Field holds
   for x being Element of suppf(F) holds
   x = compf(F).(compf(F).x)
proof
   let F be Field;
   let x be Element of suppf(F);
     x = odf(F).[x,ndf(F)] by Th13
         .= odf(F).[x,odf(F).[compf(F).x,compf(F).(compf(F).x)]] by Def8
         .= odf(F).[odf(F).[x,compf(F).x],compf(F).(compf(F).x)] by Th11
         .= odf(F).[ndf(F),compf(F).(compf(F).x)] by Def8
         .= compf(F).(compf(F).x) by Th13;
   hence thesis;
end;

theorem Th28:
    for F being Field holds
    for a,b being Element of suppf(F) holds
    (odf(F).[a,b] is Element of suppf(F) &
    omf(F).[a,b] is Element of suppf(F) &
    compf(F).a is Element of suppf(F))
proof
    let F be Field;
    let a,b be Element of suppf(F);
      [a,b] in [:suppf(F),suppf(F):] by ZFMISC_1:def 2;
    hence thesis by REALSET1:10;
end;

theorem Th29:
   for F being Field holds
   for a,b,c being Element of suppf(F) holds
   omf(F).[a,odf(F).[b,compf(F).c]] =
   odf(F).[omf(F).[a,b],compf(F).(omf(F).[a,c])]
proof
   let F be Field;
   let a,b,c be Element of suppf(F);
     omf(F).[a,c] is Element of suppf(F) by Th28;
then A1:odf(F).[omf(F).[a,c],compf(F).(omf(F).[a,c])] = ndf(F) by Def8;
A2:odf(F).[b,compf(F).c] is Element of suppf(F) by Th28;
then A3:omf(F).[a,odf(F).[b,compf(F).c]] is Element of suppf(F) by Th28;
A4:omf(F).[a,c] is Element of suppf(F) by Th28;
then A5:compf(F).(omf(F).[a,c]) is Element of suppf(F) by Th28;
A6:odf(F).[odf(F).[b,compf(F).c],c] =
   odf(F).[b,odf(F).[compf(F).c,c]] by Th11
   .= odf(F).[b,odf(F).[c,compf(F).c]] by Th12
   .= odf(F).[b,ndf(F)] by Def8
   .= b by Th13;
     omf(F).[a,odf(F).[b,compf(F).c]] =odf(F).[omf(F).[a,odf(F).[b,compf(F).c]]
,
      odf(F).[omf(F).[a,c],compf(F).(omf(F).[a,c])]] by A1,A3,Th13
   .= odf(F).[odf(F).[omf(F).[a,odf(F).[b,compf(F).c]],
      omf(F).[a,c]],compf(F).(omf(F).[a,c])] by A3,A4,A5,Th11
   .= odf(F).[omf(F).[a,b],compf(F).(omf(F).[a,c])] by A2,A6,Th10;
   hence thesis;
end;

theorem Th30:
   for F being Field holds
   for a,b,c being Element of suppf(F) holds
   omf(F).[odf(F).[a,compf(F).b],c] =
   odf(F).[omf(F).[a,c],compf(F).(omf(F).[b,c])]
proof
   let F be Field;
   let a,b,c be Element of suppf(F);
     omf(F).[b,c] is Element of suppf(F) by Th28;
then A1:odf(F).[omf(F).[b,c],compf(F).(omf(F).[b,c])] = ndf(F) by Def8;
A2:odf(F).[a,compf(F).b] is Element of suppf(F) by Th28;
then A3:omf(F).[odf(F).[a,compf(F).b],c] is Element of suppf(F) by Th28;
A4:omf(F).[b,c] is Element of suppf(F) by Th28;
then A5:compf(F).(omf(F).[b,c]) is Element of suppf(F) by Th28;
A6:odf(F).[odf(F).[a,compf(F).b],b] =
   odf(F).[a,odf(F).[compf(F).b,b]] by Th11
   .= odf(F).[a,odf(F).[b,compf(F).b]] by Th12
   .= odf(F).[a,ndf(F)] by Def8
   .= a by Th13;
     omf(F).[odf(F).[a,compf(F).b],c] =odf(F).[omf(F).[odf(F).[a,compf(F).b],c]
,
      odf(F).[omf(F).[b,c],compf(F).(omf(F).[b,c])]] by A1,A3,Th13
   .= odf(F).[odf(F).[omf(F).[odf(F).[a,compf(F).b],c],
      omf(F).[b,c]],compf(F).(omf(F).[b,c])] by A3,A4,A5,Th11
   .= odf(F).[omf(F).[a,c],compf(F).(omf(F).[b,c])] by A2,A6,Th10;
   hence thesis;
end;

theorem Th31:
   for F being Field holds
   for a being Element of suppf(F) holds omf(F).[a,ndf(F)] = ndf(F)
proof
   let F be Field;
   let a be Element of suppf(F);
     nmf(F) in (suppf(F)\{ndf F});
then A1:nmf(F) is Element of suppf(F) by XBOOLE_0:def 4;
then A2:omf(F).[a,nmf(F)] is Element of suppf(F) by Th28;
      omf(F).[a,ndf(F)] = omf(F).[a,odf(F).[nmf(F),compf(F).nmf(F)]]
            by A1,Def8
    .= odf(F).[omf(F).[a,nmf(F)],compf(F).(omf(F).[a,nmf(F)])] by A1,Th29
    .= ndf(F) by A2,Def8;
    hence thesis;
end;

theorem Th32:
   for F being Field holds
   for a being Element of suppf(F) holds omf(F).[ndf(F),a] = ndf(F)
proof
   let F be Field;
   let a be Element of suppf(F);
     nmf(F) in suppf(F)\{ndf(F)};
then A1:nmf(F) is Element of suppf(F) by XBOOLE_0:def 4;
   then A2:omf(F).[nmf(F),a] is Element of suppf(F) by Th28;
     omf(F).[ndf(F),a] = omf(F).[odf(F).[nmf(F),compf(F).nmf(F)],a] by A1,Def8
    .= odf(F).[omf(F).[nmf(F),a],compf(F).(omf(F).[nmf(F),a])] by A1,Th30
    .= ndf(F) by A2,Def8;
   hence thesis;
end;

theorem
     for F being Field,
       a,b being Element of suppf(F) holds
   compf(F).(omf(F).[a,b]) = omf(F).[a,compf(F).b]
   proof
      let F be Field,
          a,b be Element of suppf(F);
   A1:omf(F).[a,b] is Element of suppf(F) by Th28;
   A2:omf(F).[a,compf(F).b] is Element of suppf(F) by Th28;
        odf(F).[omf(F).[a,b],omf(F).[a,compf(F).b]]
         = omf(F).[a,odf(F).[b,compf(F).b]] by Th10
        .= omf(F).[a,ndf(F)] by Def8
        .= ndf(F) by Th31;
      hence thesis by A1,A2,Th26;
   end;

theorem Th34:
   for F being Field holds omf(F).[nmf(F),ndf(F)] = ndf(F)
proof
   let F be Field;
     nmf(F) in suppf(F)\{ndf(F)};
   then nmf(F) is Element of suppf(F) by XBOOLE_0:def 4;
   hence thesis by Th31;
end;

theorem Th35:
   for F being Field holds omf(F).[ndf(F),nmf(F)] = ndf(F)
proof
   let F be Field;
     nmf(F) in suppf(F)\{ndf(F)};
   then nmf(F) is Element of suppf(F) by XBOOLE_0:def 4;
   hence thesis by Th32;
end;

theorem
    for F being Field,
       a,b being Element of suppf(F) holds
   omf(F).[a,b] is Element of suppf(F) by Th28;

theorem Th37:
   for F being Field,
       a,b,c being Element of suppf(F) holds
   omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]
proof
   let F be Field,
       a,b,c be Element of suppf(F);
A1:a = ndf(F) or b = ndf(F) or c = ndf(F) or
   (a is Element of suppf(F)\{ndf(F)} &
    b is Element of suppf(F)\{ndf(F)} &
    c is Element of suppf(F)\{ndf(F)}) by ZFMISC_1:64;
A2: omf(F).[a,b] is Element of suppf(F) by Th28;
A3: omf(F).[b,c] is Element of suppf(F) by Th28;
A4:a = ndf(F) implies omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]
   proof
      assume
   A5:a = ndf(F);
      hence omf(F).[omf(F).[a,b],c] = omf(F).[ndf(F),c] by Th32
                            .= ndf(F) by Th32
                            .= omf(F).[a,omf(F).[b,c]] by A3,A5,Th32;
   end;
A6:b = ndf(F) implies omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]
   proof
      assume
   A7:b = ndf(F);
      hence omf(F).[omf(F).[a,b],c] = omf(F).[ndf(F),c] by Th31
                            .= ndf(F) by Th32
                            .= omf(F).[a,ndf(F)] by Th31
                            .= omf(F).[a,omf(F).[b,c]] by A7,Th32;
   end;
     c = ndf(F) implies omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]
   proof
      assume
   A8:c = ndf(F);
      hence omf(F).[omf(F).[a,b],c] = ndf(F) by A2,Th31
                            .= omf(F).[a,ndf(F)] by Th31
                            .= omf(F).[a,omf(F).[b,c]] by A8,Th31;
   end;
   hence thesis by A1,A4,A6,Th20;
end;

theorem
     for F being Field,
       a,b being Element of suppf(F) holds
   omf(F).[a,b] = omf(F).[b,a]
proof
   let F be Field,
       a,b be Element of suppf(F);
A1:a = ndf(F) or b = ndf(F) or
   (a is Element of suppf(F)\{ndf(F)} &
    b is Element of suppf(F)\{ndf(F)}) by ZFMISC_1:64;
A2:a = ndf(F) implies omf(F).[a,b] = omf(F).[b,a]
   proof
      assume
   A3:a = ndf(F);
      then omf(F).[a,b] = ndf(F) by Th32
                  .= omf(F).[b,a] by A3,Th31;
      hence thesis;
   end;
     b = ndf(F) implies omf(F).[a,b] = omf(F).[b,a]
   proof
      assume
   A4:b = ndf(F);
      then omf(F).[a,b] = ndf(F) by Th31
                  .= omf(F).[b,a] by A4,Th32;
      hence thesis;
   end;
   hence thesis by A1,A2,Th21;
end;

theorem Th39:
   for F being Field,
       a being Element of suppf(F) holds
   omf(F).[a,nmf(F)] = a & omf(F).[nmf(F),a] = a
proof
   let F be Field,
       a be Element of suppf(F);
     a = ndf(F) or a is Element of suppf(F)\{ndf(F)} by ZFMISC_1:64;
   hence thesis by Th22,Th34,Th35;
end;

definition :: reverse element
  let F be Field;
  func revf(F) -> Function of suppf(F)\{ndf(F)},suppf(F)\{ndf(F)} means
:Def9: for x being Element of suppf(F)\{ndf(F)} holds
        omf(F).[x,it.x] = nmf(F);
existence
proof
  defpred Z[set,set] means omf(F).[$1,$2] = nmf(F);
   A1:for x being set st x in suppf(F)\{ndf(F)} ex y being set st
          y in suppf(F)\{ndf(F)} & Z[x,y]
      proof
         let x be set;
         assume x in suppf(F)\{ndf(F)};
         then consider y being Element of suppf(F)\{ndf(F)} such that
      A2:omf(F).[x,y] = nmf(F) & omf(F).[y,x] = nmf(F) by Th23;
         reconsider y as set;
         take y;
         thus thesis by A2;
      end;
      ex C being Function of suppf(F)\{ndf(F)},suppf(F)\{ndf(F)} st
    for x being set st x in suppf(F)\{ndf(F)} holds Z[x,C.x] from FuncEx1(A1);
    then consider C being Function of suppf(F)\{ndf(F)},suppf(F)\{ndf(F)} such
that
A3:for x being set st x in suppf(F)\{ndf(F)} holds omf(F).[x,C.x] = nmf(F);
    take C;
    thus thesis by A3;
end;
uniqueness
proof
   let C1,C2 be Function of suppf(F)\{ndf(F)},suppf(F)\{ndf(F)} such that
A4:for x being Element of suppf(F)\{ndf(F)} holds
       omf(F).[x,C1.x] = nmf(F) and
A5:for x being Element of suppf(F)\{ndf(F)} holds
       omf(F).[x,C2.x] = nmf(F);
     for x being set st x in suppf(F)\{ndf(F)} holds C1.x = C2.x
      proof
         let x be set;
         assume
     A6:x in suppf(F)\{ndf(F)};
      then A7:C1.x is Element of suppf(F)\{ndf(F)} by FUNCT_2:7;
      A8:C2.x is Element of suppf(F)\{ndf(F)} by A6,FUNCT_2:7;
           C1.x = omf(F).[C1.x,nmf(F)] by A7,Th22
             .= omf(F).[C1.x,omf(F).[x,C2.x]] by A5,A6
             .= omf(F).[omf(F).[C1.x,x],C2.x] by A6,A7,A8,Th20
             .= omf(F).[omf(F).[x,C1.x],C2.x] by A6,A7,Th21
             .= omf(F).[nmf(F),C2.x] by A4,A6
             .= C2.x by A8,Th22;
         hence thesis;
      end;
      hence thesis by FUNCT_2:18;
end;
end;

canceled 2;

theorem
     for F being Field holds
   for x,y being Element of suppf(F)\{ndf(F)} holds
      omf(F).[x,y] = nmf(F) implies y = revf(F).x
proof
   let F be Field;
   let x,y be Element of suppf(F)\{ndf(F)};
   assume
A1:omf(F).[x,y] = nmf(F);
     y = omf(F).[y,nmf(F)] by Th22
         .= omf(F).[y,omf(F).[x,revf(F).x]] by Def9
         .= omf(F).[omf(F).[y,x],revf(F).x] by Th20
         .= omf(F).[nmf(F),revf(F).x] by A1,Th21
         .= revf(F).x by Th22;
   hence thesis;
end;

theorem
     for F being Field holds
   for x being Element of suppf(F)\{ndf(F)} holds
      x =revf(F).(revf(F).x)
proof
   let F be Field;
   let x be Element of suppf(F)\{ndf(F)};
     x = omf(F).[x,nmf(F)] by Th22
         .= omf(F).[x,omf(F).[revf(F).x,revf(F).(revf(F).x)]] by Def9
         .= omf(F).[omf(F).[x,revf(F).x],revf(F).(revf(F).x)] by Th20
         .= omf(F).[nmf(F),revf(F).(revf(F).x)] by Def9
         .= revf(F).(revf(F).x) by Th22;
   hence thesis;
end;

theorem
     for F being Field holds
   for a,b being Element of suppf(F)\{ndf(F)} holds
   omf(F).[a,b] is Element of suppf(F)\{ndf(F)} &
   revf(F).a is Element of suppf(F)\{ndf(F)}
proof
   let F be Field;
   let a,b be Element of suppf(F)\{ndf(F)};
     [a,b] in [:suppf(F)\{ndf(F)},suppf(F)\{ndf(F)}:] by ZFMISC_1:def 2;
   hence thesis by REALSET1:def 18;
end;

theorem
     for F being Field holds
   for a,b,c being Element of suppf(F) holds
   odf(F).[a,b] = odf(F).[a,c] implies b = c
proof
   let F be Field;
   let a,b,c be Element of suppf(F);
   assume
A1:odf(F).[a,b] = odf(F).[a,c];
     b = odf(F).[ndf(F),b] by Th13
    .= odf(F).[odf(F).[a,compf(F).a],b] by Def8
    .= odf(F).[odf(F).[compf(F).a,a],b] by Th12
    .= odf(F).[compf(F).a,odf(F).[a,c]] by A1,Th11
    .= odf(F).[odf(F).[compf(F).a,a],c] by Th11
    .= odf(F).[odf(F).[a,compf(F).a],c] by Th12
    .= odf(F).[ndf(F),c] by Def8
    .= c by Th13;
   hence thesis;
end;

theorem
     for F being Field holds
   for a being Element of suppf(F)\{ndf(F)} holds
   for b,c being Element of suppf(F) holds
   omf(F).[a,b] = omf(F).[a,c] implies b = c
proof
   let F be Field;
   let a be Element of suppf(F)\{ndf(F)};
   let b,c be Element of suppf(F);
   assume
A1:omf(F).[a,b] = omf(F).[a,c];
A2:revf(F).a is Element of suppf(F) by XBOOLE_0:def 4;
A3:a is Element of suppf(F) by XBOOLE_0:def 4;
     b = omf(F).[nmf(F),b] by Th39
    .= omf(F).[omf(F).[a,revf(F).a],b] by Def9
    .= omf(F).[omf(F).[revf(F).a,a],b] by Th21
    .= omf(F).[(revf(F).a),omf(F).[a,c]] by A1,A2,A3,Th37
    .= omf(F).[omf(F).[revf(F).a,a],c] by A2,A3,Th37
    .= omf(F).[omf(F).[a,revf(F).a],c] by Th21
    .= omf(F).[nmf(F),c] by Def9
    .= c by Th39;
   hence thesis;
end;

Back to top