REALSET2

:: Properties of Fields
::  by J\'ozef Bia{\l}as
::
:: Received June 20, 1990
:: Copyright (c) 1990-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 BINOP_1, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, XBOOLE_0, ZFMISC_1,
      TARSKI, FUNCT_7, SUBSET_1, FUNCT_1, ALGSTR_0, ARYTM_3, SUPINF_2,
      REALSET1, VECTSP_1, STRUCT_0, MESFUNC1, RLVECT_1, LATTICES, ARYTM_1,
      REALSET2, MEMBERED;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
      ORDINAL1, NUMBERS, REALSET1, FUNCOP_1, FUNCT_2, BINOP_1, FUNCT_4,
      FUNCT_7, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1;
 constructors RLVECT_1, BINOP_1, FUNCT_4, REALSET1, FUNCT_7, VECTSP_1,
      RELSET_1, MEMBERED, GROUP_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, RLVECT_1,
      VECTSP_1, ORDINAL1, ALGSTR_0, ZFMISC_1, CARD_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions RLVECT_1, STRUCT_0, VECTSP_1, ALGSTR_0;
 equalities TARSKI, REALSET1, BINOP_1, STRUCT_0, FUNCOP_1, ALGSTR_0, ORDINAL1;
 expansions RLVECT_1, TARSKI, MEMBERED, VECTSP_1;
 theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, ENUMSET1, REALSET1, VECTSP_1,
      RELSET_1, XBOOLE_0, RLVECT_1, FUNCT_4, FUNCOP_1, CARD_1, XBOOLE_1,
      STRUCT_0, GROUP_1, ALGSTR_0, XTUPLE_0, SUBSET_1;
 schemes FUNCT_2;

begin

definition
  func add_2 -> BinOp of 2 equals
  ((0,0) .--> 0) +* ((0,1).-->1) +* ((1,0).-->1) +* ((1,1).-->0);
  coherence
  proof
    set f2 = ((0,0).-->0) +* ((0,1).-->1), f1 = f2 +* ((1,0).-->1), f = f1 +*(
    (1,1).-->0);
A1: dom f = dom f1 \/ dom((1,1).-->0) by FUNCT_4:def 1
      .= dom f1 \/ {[1,1]} by FUNCOP_1:13
      .= dom f2 \/ dom((1,0).-->1) \/ {[1,1]} by FUNCT_4:def 1
      .= dom f2 \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= dom((0,0) .--> 0) \/ dom ((0,1).-->1) \/ {[1,0]} \/ {[1,1]} by
FUNCT_4:def 1
      .= dom((0,0) .--> 0) \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= {[0,0]} \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= {[0,0],[0,1]} \/ {[1,0]} \/ {[1,1]} by ENUMSET1:1
      .= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
      .= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
      .= [:2,2:] by CARD_1:50,ZFMISC_1:122;
A2: 1 c= 2 by CARD_1:49,50,ZFMISC_1:7;
    rng ((0,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
    then
A3: rng ((0,0).-->0) c= 2 by A2;
A4: {1} c= 2 by CARD_1:50,ZFMISC_1:7;
    rng ((0,1).-->1) c= {1} by FUNCOP_1:13;
    then rng ((0,1).-->1) c= 2 by A4;
    then
A5: rng ((0,0).-->0) \/ rng ((0,1).-->1) c= 2 by A3,XBOOLE_1:8;
    rng ((1,0).-->1) c= {1} by FUNCOP_1:13;
    then
A6: rng ((1,0).-->1) c= 2 by A4;
    rng f2 c= rng ((0,0).-->0) \/ rng ((0,1).-->1) by FUNCT_4:17;
    then rng f2 c= 2 by A5;
    then
A7: rng f2 \/ rng ((1,0).-->1) c= 2 by A6,XBOOLE_1:8;
    rng ((1,1).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
    then
A8: rng ((1,1).-->0) c= 2 by A2;
    rng f1 c= rng f2 \/ rng ((1,0).-->1) by FUNCT_4:17;
    then rng f1 c= 2 by A7;
    then
A9: rng f1 \/ rng ((1,1).-->0) c= 2 by A8,XBOOLE_1:8;
    rng f c= rng f1 \/ rng ((1,1).-->0) by FUNCT_4:17;
    then rng f c= 2 by A9;
    hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
  end;
  func mult_2 -> BinOp of 2 equals
  ((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0) +* ((1,1).-->1);
  coherence
  proof
A10: rng ((1,1).-->1) c= {1} by FUNCOP_1:13;
    {1} c= 2 by CARD_1:50,ZFMISC_1:7;
    then
A11: rng ((1,1).-->1) c= 2 by A10;
    set f2 = ((0,0).-->0) +* ((0,1).-->0), f1 = f2 +* ((1,0).-->0), f = f1 +*
    ((1,1).-->1);
A12: dom f = dom f1 \/ dom ((1,1).-->1) by FUNCT_4:def 1
      .= dom f1 \/ {[1,1]} by FUNCOP_1:13
      .= dom f2 \/ dom ((1,0).-->0) \/ {[1,1]} by FUNCT_4:def 1
      .= dom f2 \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= dom(((0,0).-->0)) \/ dom ((0,1).-->0) \/ {[1,0]} \/ {[1,1]} by
FUNCT_4:def 1
      .= dom(((0,0).-->0)) \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= {[0,0]} \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
      .= {[0,0],[0,1]} \/ {[1,0]} \/ {[1,1]} by ENUMSET1:1
      .= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
      .= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
      .= [:2,2:] by CARD_1:50,ZFMISC_1:122;
A13: 1 c= 2 by CARD_1:49,50,ZFMISC_1:7;
    rng ((0,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
    then
A14: rng ((0,0).-->0) c= 2 by A13;
    rng ((0,1).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
    then rng ((0,1).-->0) c= 2 by A13;
    then
A15: rng ((0,0).-->0) \/ rng ((0,1).-->0) c= 2 by A14,XBOOLE_1:8;
    rng ((1,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
    then
A16: rng ((1,0).-->0) c= 2 by A13;
    rng f2 c= rng ((0,0).-->0) \/ rng ((0,1).-->0) by FUNCT_4:17;
    then rng f2 c= 2 by A15;
    then
A17: rng f2 \/ rng ((1,0).-->0) c= 2 by A16,XBOOLE_1:8;
    rng f1 c= rng f2 \/ rng ((1,0).-->0) by FUNCT_4:17;
    then rng f1 c= 2 by A17;
    then
A18: rng f1 \/ rng ((1,1).-->1) c= 2 by A11,XBOOLE_1:8;
    rng f c= rng f1 \/ rng ((1,1).-->1) by FUNCT_4:17;
    then rng f c= 2 by A18;
    hence thesis by A12,FUNCT_2:def 1,RELSET_1:4;
  end;
end;

reserve x,y for set;

:: Properties of fields

set x = In(0,2), y = In(1,2);

Lm1: 1 in 2 by CARD_1:50,TARSKI:def 2;

Lm2: 0 in 2 by CARD_1:50,TARSKI:def 2;
then

Lm3: x = 0 by SUBSET_1:def 8;

Lm4: y = 1 by Lm1,SUBSET_1:def 8;

set Z = 2;
reconsider A = Z as non trivial set by Lm1,Lm2,ZFMISC_1:def 10;
reconsider nd = x as Element of A;

Lm5: dom ((1,1).-->0) = {[1,1]} by FUNCOP_1:13;
Lm6: dom(((1,0).-->1)) = {[1,0]} by FUNCOP_1:13;
Lm7: dom ((0,1).-->1) = {[0,1]} by FUNCOP_1:13;

Lm8: add_2.(x,x) = x
proof
  [x,x] <> [0,1] by Lm3,XTUPLE_0:1;
  then
A1: not [x,x] in dom ((0,1).-->1) by Lm7,TARSKI:def 1;
  [x,x] <> [1,0] by Lm3,XTUPLE_0:1;
  then
A2: not [x,x] in dom(((1,0).-->1)) by Lm6,TARSKI:def 1;
  [x,x] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [x,x] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
  hence add_2.(x,x) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(x,x) by
FUNCT_4:11
    .= (((0,0).-->0) +* ((0,1).-->1)).(x,x) by A2,FUNCT_4:11
    .= (((0,0).-->0)).(x,x) by A1,FUNCT_4:11
    .= x by Lm3,FUNCOP_1:71;
end;

Lm9: add_2.(x,y) = y
proof
  [x,y] <> [1,0] by Lm3,XTUPLE_0:1;
  then
A1: not [x,y] in dom(((1,0).-->1)) by Lm6,TARSKI:def 1;
A2: [x,y] in dom(((0,1).-->1)) by Lm3,Lm4,Lm7,TARSKI:def 1;
  [x,y] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [x,y] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
  hence add_2.(x,y) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(x,y) by
FUNCT_4:11
    .= (((0,0).-->0) +* ((0,1).-->1)).(x,y) by A1,FUNCT_4:11
    .= (((0,1).-->1)).(x,y) by A2,FUNCT_4:13
    .= y by Lm3,Lm4,FUNCOP_1:71;
end;

Lm10: add_2.(y,x) = y
proof
A1: [y,x] in dom(((1,0).-->1)) by Lm3,Lm4,Lm6,TARSKI:def 1;
  [y,x] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [y,x] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
  hence add_2.(y,x) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(y,x) by
FUNCT_4:11
    .= (((1,0).-->1)).(y,x) by A1,FUNCT_4:13
    .= y by Lm3,Lm4,FUNCOP_1:71;
end;

Lm11: add_2.(y,y) = x
proof
  [y,y] in dom ((1,1).-->0) by Lm4,Lm5,TARSKI:def 1;
  hence add_2.(y,y) = (((1,1).-->0)).(y,y) by FUNCT_4:13
    .= x by Lm3,Lm4,FUNCOP_1:71;
end;

Lm12: dom ((1,1).-->1) = {[1,1]} by FUNCOP_1:13;

Lm13: dom ((1,0).-->0) = {[1,0]} by FUNCOP_1:13;

Lm14: dom ((0,1).-->0) = {[0,1]} by FUNCOP_1:13;

Lm15: mult_2.(x,x) = x
proof
  [x,x] <> [0,1] by Lm3,XTUPLE_0:1;
  then
A1: not [x,x] in dom ((0,1).-->0) by Lm14,TARSKI:def 1;
  [x,x] <> [1,0] by Lm3,XTUPLE_0:1;
  then
A2: not [x,x] in dom ((1,0).-->0) by Lm13,TARSKI:def 1;
  [x,x] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [x,x] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
  hence mult_2.(x,x) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(x,x) by
FUNCT_4:11
    .= (((0,0).-->0) +* ((0,1).-->0)).(x,x) by A2,FUNCT_4:11
    .= (((0,0).-->0)).(x,x) by A1,FUNCT_4:11
    .= x by Lm3,FUNCOP_1:71;
end;

Lm16: mult_2.(x,y) = x
proof
  [x,y] <> [1,0] by Lm3,XTUPLE_0:1;
  then
A1: not [x,y] in dom ((1,0).-->0) by Lm13,TARSKI:def 1;
A2: [x,y] in dom ((0,1).-->0) by Lm3,Lm4,Lm14,TARSKI:def 1;
  [x,y] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [x,y] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
  hence mult_2.(x,y) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(x,y) by
FUNCT_4:11
    .= (((0,0).-->0) +* ((0,1).-->0)).(x,y) by A1,FUNCT_4:11
    .= (((0,1).-->0)).(x,y) by A2,FUNCT_4:13
    .= x by Lm3,Lm4,FUNCOP_1:71;
end;

Lm17: mult_2.(y,x) = x
proof
A1: [y,x] in dom ((1,0).-->0) by Lm3,Lm4,Lm13,TARSKI:def 1;
  [y,x] <> [1,1] by Lm3,XTUPLE_0:1;
  then not [y,x] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
  hence mult_2.(y,x) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(y,x) by
FUNCT_4:11
    .= (((1,0).-->0)).(y,x) by A1,FUNCT_4:13
    .= x by Lm3,Lm4,FUNCOP_1:71;
end;

Lm18: mult_2.(y,y) = y
proof
  [y,y] in dom ((1,1).-->1) by Lm4,Lm12,TARSKI:def 1;
  hence mult_2.(y,y) = (((1,1).-->1)).(y,y) by FUNCT_4:13
    .= y by Lm4,FUNCOP_1:71;
end;

set om = mult_2;

Lm19: A\{x}={y} by Lm3,Lm4,CARD_1:50,ZFMISC_1:17; then
Lm20: [:A\{x},A\{x}:] = {[y,y]} by ZFMISC_1:29;
Lm21: 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 Lm20,TARSKI:def 1;
  hence thesis by Lm18,Lm19,TARSKI:def 1;
end;

reconsider nm = y as Element of A\{nd} by Lm19,TARSKI:def 1;
reconsider od0=add_2 as BinOp of A;
reconsider om0=om as BinOp of A;

Lm22: for a,b,d being Element of A holds add_2.(add_2.(a,b),d) = add_2.(a,
add_2.(b,d))
proof
  let a,b,d be Element of A;
A1: a = x or a = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
A2: b = x or b = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
A3: d = x or d = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
  per cases by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
  suppose
    a = x;
    hence thesis by A2,A3,Lm8,Lm9,Lm10,Lm11;
  end;
  suppose
    b = x;
    hence thesis by A1,A3,Lm8,Lm9,Lm10;
  end;
  suppose
    d = x;
    hence thesis by A1,A2,Lm8,Lm9,Lm10,Lm11;
  end;
  suppose
    a = y & b = y & d = y;
    hence thesis by Lm9,Lm10,Lm11;
  end;
end;

reconsider dL=doubleLoopStr(#A,od0,om0,nm,nd#) as non empty doubleLoopStr;

Lm23: for a being Element of dL holds a + 0.dL = a
proof
  let a be Element of dL;
  a=x or a=y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
  hence thesis by Lm8,Lm10;
end;

Lm24: for a,b,c being Element of dL holds a+b+c = a+(b+c) by Lm22;

Lm25: for a,b being Element of dL holds a+b = b+a
proof
  let a,b be Element of dL;
  a=x & b=x or a=x & b=y or a=y & b=x or a=y & b=y by Lm3,Lm4,CARD_1:50
,TARSKI:def 2;
  hence thesis by Lm9,Lm10;
end;

reconsider om1=om as (A\{nd})-subsetpreserving BinOp of A
  by Lm21,REALSET1:def 4;

Lm26: for B being non empty set, P being BinOp of B, e being Element of B st B
= A\{nd} & e = nm holds addLoopStr(#B,P,e#) is AbGroup
proof
  let B be non empty set, P be BinOp of B, e be Element of B;
  assume that
A1: B = A\{nd} and
A2: e = nm;
A3: addLoopStr(#B,P,e#) is right_complementable
  proof
    let a be Element of addLoopStr(#B,P,e#);
    take a;
    thus thesis by A1,A2,Lm19,TARSKI:def 1;
  end;
  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;
A4: b = y by A1,Lm19,TARSKI:def 1;
A5: c = y by A1,Lm19,TARSKI:def 1;
    a = y by A1,Lm19,TARSKI:def 1;
    hence thesis by A1,A4,A5,Lm19,TARSKI:def 1;
  end;
  then
A6: for a,b,c being Element of addLoopStr(#B,P,e#) holds a+b+c = a+(b+c);
A7: for a,b being Element of addLoopStr(#B,P,e#) holds a+b = b+a
  proof
    let a,b be Element of addLoopStr(#B,P,e#);
    a = y by A1,Lm19,TARSKI:def 1;
    hence thesis by A1,Lm19,TARSKI:def 1;
  end;
  for a being Element of addLoopStr(#B,P,e#) holds a+0.addLoopStr(#B,P,e#) = a
  proof
    let a be Element of addLoopStr(#B,P,e#);
    a = y by A1,Lm19,TARSKI:def 1;
    hence thesis by A1,Lm19,TARSKI:def 1;
  end;
  hence thesis by A3,A6,A7,RLVECT_1:def 2,def 3,def 4;
end;

Lm27: for a,b,d being Element of dL holds a*(b+d) = a*b+a*d & (b+d)*a = b*a+d*
a
proof
  let a,b,d be Element of dL;
A1: 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
Lm3,Lm4,CARD_1:50,TARSKI:def 2;
  hence a*(b+d) = a*b+a*d by Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
  thus thesis by A1,Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
end;

definition
  func dL-Z_2 -> doubleLoopStr equals
  doubleLoopStr(#2,add_2,mult_2,In(1,2),In(0,2)#);
  coherence;
end;

registration
  cluster dL-Z_2 -> strict non empty non degenerated;
  coherence
  proof
    thus dL-Z_2 is strict;
    thus the carrier of dL-Z_2 is non empty;
    0 in 2 by CARD_1:50,TARSKI:def 2;
    then
A1: 0.dL-Z_2 = 0 by SUBSET_1:def 8;
    1 in 2 by CARD_1:50,TARSKI:def 2;
    hence 0.dL-Z_2 <> 1.dL-Z_2 by A1,SUBSET_1:def 8;
  end;
end;

registration
  cluster dL-Z_2 -> add-associative distributive;
  coherence
  proof
    for a,b,c being Element of dL-Z_2 holds a+b+c = a+(b+c) by Lm22;
    hence dL-Z_2 is add-associative;
    thus dL-Z_2 is distributive
    proof
      let a,b,d be Element of dL-Z_2;
A1:   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 Lm3,Lm4,CARD_1:50,TARSKI:def 2;
      hence a*(b+d) = a*b+a*d by Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
      thus thesis by A1,Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
    end;
  end;
end;

registration
  cluster add-associative for non trivial strict doubleLoopStr;
  existence
  proof
    take dL-Z_2;
    thus thesis;
  end;
end;

registration
  cluster the carrier of dL-Z_2 -> natural-membered;
  coherence by CARD_1:50,TARSKI:def 2;
end;

registration
  cluster empty for Element of dL-Z_2;
  existence
  proof
    reconsider z = 0 as Element of dL-Z_2 by CARD_1:50,TARSKI:def 2;
    take z;
    thus thesis;
  end;
  cluster non empty for Element of dL-Z_2;
  existence
  proof
    reconsider z = 1 as Element of dL-Z_2 by CARD_1:50,TARSKI:def 2;
    take z;
    thus thesis;
  end;
end;

definition
  let L be doubleLoopStr;
  attr L is Field-like means  :Def4:
  the multF of L is ((the carrier of L)\{0.L})-subsetpreserving &
  for B being non empty set, P being BinOp of B, e being Element of B
  holds B = NonZero L & e = 1.L & P = (the multF of L)||NonZero L implies
  addLoopStr(#B,P,e#) is AbGroup;
end;

registration
  let A be non empty set, od be BinOp of A, nd be Element of A,
      om be BinOp of A, nm be Element of A;
  cluster doubleLoopStr(#A,od,om,nm,nd#) -> non empty;
  coherence;
end;

Lm28: 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 addLoopStr(#B,P,e#) is AbGroup by Lm26;

registration
  cluster strict Field-like Abelian distributive add-associative right_zeroed
    right_complementable for non degenerated doubleLoopStr;
  existence
  proof
    set L = doubleLoopStr(#A,od0,om0,nm,nd#);
A1: 0.L = nd;
    1.L = nm;
    then reconsider L as non degenerated doubleLoopStr by A1,Lm3,Lm4,
STRUCT_0:def 8;
    take L;
    thus L is strict;
    thus the multF of L is ((the carrier of L) \ {0.L})-subsetpreserving
      by Lm28;
    L is right_complementable
    proof
      let a be Element of L;
      take a;
      a=x or a=y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
      hence thesis by Lm8,Lm11;
    end;
    hence thesis by Lm23,Lm24,Lm25,Lm26,Lm27;
  end;
end;

registration
  cluster add-associative right_zeroed right_complementable Abelian
    commutative associative well-unital distributive almost_left_invertible ->
    Field-like for non degenerated doubleLoopStr;
  coherence
  proof
    let L be non degenerated doubleLoopStr;
    set B = NonZero L;
    assume
A1: L is add-associative right_zeroed right_complementable Abelian
    commutative associative well-unital distributive almost_left_invertible;
A2: for y being set st y in [:B,B:] holds (the multF of L).y in B
    proof
      let z be set;
      assume z in [:B,B:];
      then consider x,y being object such that
A3:   x in B and
A4:   y in B and
A5:   z = [x,y] by ZFMISC_1:84;
      reconsider x,y as Element of L by A3,A4;
      not y in {0.L} by A4,XBOOLE_0:def 5;
      then
A6:   y <> 0.L by TARSKI:def 1;
      not x in {0.L} by A3,XBOOLE_0:def 5;
      then x <> 0.L by TARSKI:def 1;
      then x*y <> 0.L by A1,A6,VECTSP_1:12;
      then not x*y in {0.L} by TARSKI:def 1;
      hence thesis by A5,XBOOLE_0:def 5;
    end;
    hence the multF of L is ((the carrier of L)\{0.L})-subsetpreserving
      by REALSET1:def 4;
    reconsider om = the multF of L as
      ((the carrier of L)\{0.L})-subsetpreserving BinOp of L by A2,
         REALSET1:def 4;
    let B be non empty set, P be BinOp of B, e be Element of B such that
A7: B = NonZero L and
A8: e = 1.L and
A9: P = (the multF of L)||NonZero L;
    set K = addLoopStr(#B,P,e#);
A10: K is Abelian
    proof
      let v,w be Element of K;
      reconsider a=v, b=w as Element of L by A7,XBOOLE_0:def 5;
A11:  [w,v] in [:B,B:];
      [v,w] in [:B,B:];
      hence v + w = a*b by A7,A9,FUNCT_1:49
        .= b*a by A1,GROUP_1:def 12
        .= w + v by A7,A9,A11,FUNCT_1:49;
    end;
A12: K is right_complementable
    proof
      let v be Element of K;
      reconsider a=v as Element of L by A7,XBOOLE_0:def 5;
      not a in {0.L} by A7,XBOOLE_0:def 5;
      then a <> 0.L by TARSKI:def 1;
      then consider b being Element of L such that
A13:  b*a = 1.L by A1;
A14:  a*b = 1.L by A1,A13,GROUP_1:def 12;
      then b <> 0.L by A1,VECTSP_1:6;
      then not b in {0.L} by TARSKI:def 1;
      then reconsider w=b as Element of K by A7,XBOOLE_0:def 5;
      take w;
      [v,w] in [:B,B:];
      hence thesis by A7,A8,A9,A14,FUNCT_1:49;
    end;
A15: K is add-associative
    proof
      let u,v,w be Element of K;
      reconsider a=u, b=v, c =w as Element of L by A7,XBOOLE_0:def 5;
A16:  [v,w] in [:B,B:];
      then P.(v,w) in B by FUNCT_2:5;
      then
A17:  [u,(om||B).(v,w)] in [:B,B:] by A7,A9,ZFMISC_1:87;
A18:  [u,v] in [:B,B:];
      then P.(u,v) in B by FUNCT_2:5;
      then [(om||B).(u,v),w] in [:B,B:] by A7,A9,ZFMISC_1:87;
      hence (u + v) + w = om.((om||B).(u,v),w) by A7,A9,FUNCT_1:49
        .= (a*b)*c by A18,FUNCT_1:49
        .= a*(b*c) by A1,GROUP_1:def 3
        .= om.(u,(om||B).(v,w)) by A16,FUNCT_1:49
        .= u + (v + w) by A7,A9,A17,FUNCT_1:49;
    end;
    K is right_zeroed
    proof
      let v be Element of K;
      reconsider a=v as Element of L by A7,XBOOLE_0:def 5;
      [v,0.K] in [:B,B:];
      hence v + 0.K = a*1.L by A7,A8,A9,FUNCT_1:49
        .= v by A1;
    end;
    hence thesis by A10,A15,A12;
  end;
end;

deffunc suppf1(Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr) = the carrier of $1;

definition
  let F be Field-like Abelian distributive add-associative right_zeroed
  right_complementable non degenerated doubleLoopStr;
  func omf(F) -> ((the carrier of F) \ {0.F})-subsetpreserving BinOp of F
    equals
  the multF of F;
  coherence by Def4;
end;

theorem
  for F being Field holds the addLoopStr of F is AbGroup
proof
  let F be Field;
  set L = the addLoopStr of F;
A1: L is add-associative
  proof
    let u,v,w being Element of L;
    reconsider a=u, b=v, c = w as Element of F;
    thus (u + v) + w = (a + b) + c .= a + (b + c) by RLVECT_1:def 3
      .= u + (v + w);
  end;
A2: L is right_zeroed
  proof
    let v be Element of L;
    reconsider a=v as Element of F;
    thus v + 0.L = a + 0.F .= v;
  end;
A3: L is right_complementable
  proof
    let v be Element of L;
    reconsider a=v as Element of F;
    consider b being Element of F such that
A4: a + b = 0.F by ALGSTR_0:def 11;
    reconsider w=b as Element of L;
    take w;
    thus thesis by A4;
  end;
  L is Abelian
  proof
    let v,w be Element of L;
    reconsider a=v, b=w as Element of F;
    thus v + w = a + b .= b + a
      .= w + v;
  end;
  hence thesis by A1,A2,A3;
end;

theorem
  for F being Field, a being Element of F holds a+0.F = a & 0.F+a = a;

theorem Th3:
  for F being AbGroup, a being Element of F
  ex b being Element of F st a+b = 0.F & b+a = 0.F
proof
  let F be AbGroup, a be Element of F;
  consider b being Element of F such that
A1: a+b = 0.F by ALGSTR_0:def 11;
  take b;
  thus a+b = 0.F by A1;
  thus thesis by A1;
end;

theorem Th4:
  for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr,
      a,b,c being Element of NonZero F holds (a*b)*c = a*(b*c)
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
  right_complementable non degenerated doubleLoopStr, a,b,c be Element of
  NonZero F;
  set B = suppf1(F)\{0.F};
  set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
  then reconsider e = 1.F as Element of B by STRUCT_0:2;
  reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
  reconsider a,b,c as Element of D;
  reconsider x=a, y=b, z=c as Element of F;
A2: omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
  F}:], (suppf1(F)\{0.F}) by REALSET1:7;
  then
A3: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A4: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
  of D).(x,y)
  proof
    let x,y be Element of suppf1(F)\{0.F};
    [x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
    hence thesis by A3,FUNCT_1:47;
  end;
A5: for s,t being Element of (suppf1(F)\{0.F}) holds (the addF of D).(s,t)
is Element of (suppf1(F)\{0.F}) & omf(F).(s,t) is Element of (suppf1(F)\{0.F})
  proof
    let s,t be Element of (suppf1(F)\{0.F});
A6: [s,t] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
    consider W being Function of [:suppf1(F)\{0.F},suppf1(F)\{0.F}:], (suppf1(
    F)\{0.F}) such that
A7: W = omf(F)||(suppf1(F)\{0.F}) by A2;
    W.(s,t) is Element of (suppf1(F)\{0.F});
    hence thesis by A3,A6,A7,FUNCT_1:47;
  end;
A8: for x,y,z being Element of suppf1(F)\{0.F} holds omf(F).((the addF of D
).(x,y),z) = (the addF of D).((the addF of D).(x,y),z) & (the addF of D).(x,omf
  (F).(y,z)) = omf(F).(x,omf(F).(y,z))
  proof
    let x,y,z be Element of suppf1(F)\{0.F};
A9: omf(F).(y,z) is Element of suppf1(F)\{0.F} by A5;
    (the addF of D).(x,y) is Element of suppf1(F)\{0.F} by A5;
    hence thesis by A4,A9;
  end;
  (x*y)*z = omf(F).((the addF of D).(a,b),c) by A4
    .= a+b+c by A8
    .= a+(b+c) by RLVECT_1:def 3
    .= (the addF of D).(a,omf(F).(b,c)) by A4
    .= x*(y*z) by A8;
  hence thesis;
end;

theorem Th5:
  for F being Field-like Abelian distributive add-associative
  right_zeroed right_complementable non degenerated doubleLoopStr, a,b being
  Element of NonZero F holds a*b = b*a
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b be Element of NonZero
  F;
  set B = suppf1(F)\{0.F};
  set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
  then reconsider e = 1.F as Element of B by STRUCT_0:2;
  reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
  reconsider a,b as Element of D;
  reconsider x = a, y = b as Element of F;
  omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
  F}:], (suppf1(F)\{0.F}) by REALSET1:7;
  then
A2: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A3: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
  of D).(x,y)
  proof
    let x,y be Element of suppf1(F)\{0.F};
    [x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
    hence thesis by A2,FUNCT_1:47;
  end;
  then x*y = a+b .= b+a
    .= y*x by A3;
  hence thesis;
end;

theorem Th6:
  for F being Field-like Abelian distributive add-associative
  right_zeroed right_complementable non degenerated doubleLoopStr, a being
  Element of NonZero F holds a*1.F = a & 1.F*a = a
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of NonZero F;
  set B = suppf1(F)\{0.F};
  set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
  then reconsider e = 1.F as Element of B by STRUCT_0:2;
  reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
  reconsider a as Element of D;
  omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
  F}:], (suppf1(F)\{0.F}) by REALSET1:7;
  then
A2: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A3: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
  of D).(x,y)
  proof
    let x,y be Element of suppf1(F)\{0.F};
    [x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
    hence thesis by A2,FUNCT_1:47;
  end;
  then
A4: omf(F).(1.F,a) = 0.D + a .= a;
  omf(F).(a,1.F) = a + 0.D by A3
    .= a;
  hence thesis by A4;
end;

theorem Th7:
  for F being Field-like Abelian distributive add-associative
  right_zeroed right_complementable non degenerated doubleLoopStr, a being
  Element of NonZero F ex b being Element of NonZero F st a*b = 1.F & b*a = 1.F
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of NonZero F;
  set B = suppf1(F)\{0.F};
  set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
  then reconsider e = 1.F as Element of B by STRUCT_0:2;
  addLoopStr(#B,P,e#) is AbGroup by A1,Def4;
  then consider D being strict AbGroup such that
A2: D = addLoopStr(#B,P,e#);
  reconsider a as Element of D by A2;
  consider b being Element of D such that
A3: a+b = 0.D and
A4: b+a = 0.D by Th3;
  reconsider b as Element of NonZero F by A2;
  take b;
  omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
  F}:], (suppf1(F)\{0.F}) by REALSET1:7;
  then
A5: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
  for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
  of D).(x,y)
  proof
    let x,y be Element of suppf1(F)\{0.F};
    [x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
    hence thesis by A2,A5,FUNCT_1:47;
  end;
  hence thesis by A2,A3,A4;
end;

theorem
  for F being Field, x,y being Element of F holds x+y = 0.F implies
  y = (comp F).x
proof
  let F be Field, x,y be Element of F;
  assume x+y = 0.F;
  then y = -x by RLVECT_1:6;
  hence thesis by VECTSP_1:def 13;
end;

theorem
  for F being Field, x being Element of F holds x = (comp F).((comp F).x )
proof
  let F be Field, x be Element of F;
  thus x = --x
    .= (comp F).-x by VECTSP_1:def 13
    .= (comp F).((comp F).x) by VECTSP_1:def 13;
end;

theorem
  for F being Field, a,b being Element of (the carrier of F)holds (the
addF of F).(a,b) is Element of (the carrier of F)& omf(F).(a,b) is Element of (
  the carrier of F)& (comp F).a is Element of the carrier of F;

theorem
  for F being Field, a,b,c being Element of F holds a*(b-c) = a*b-a*c by
VECTSP_1:11;

theorem
  for F being Field, a,b,c being Element of F holds (a-b)*c = a*c-b*c by
VECTSP_1:13;

theorem
  for F being Field, a being Element of F holds a*0.F = 0.F;

theorem
  for F being Field, a being Element of F holds 0.F*a = 0.F;

theorem
  for F being Field, a,b being Element of F holds -(a*b) = a*-b by VECTSP_1:8;

theorem
  for F being Field holds 1.F*0.F = 0.F;

theorem
  for F being Field holds 0.F*1.F = 0.F;

theorem
  for F being Field, a,b being Element of (the carrier of F)holds omf(F)
  .(a,b) is Element of the carrier of F;

theorem Th19:
  for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c being
  Element of F holds (a*b)*c = a*(b*c)
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
  right_complementable non degenerated doubleLoopStr, a,b,c be Element of
  suppf1(F);
  a = 0.F or b = 0.F or c = 0.F or a is Element of NonZero F & b is
  Element of NonZero F & c is Element of NonZero F by ZFMISC_1:56;
  hence thesis by Th4;
end;

theorem Th20:
  for F being Field-like Abelian distributive add-associative
  right_zeroed right_complementable non degenerated doubleLoopStr, a,b being
  Element of F holds a*b = b*a
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b be Element of suppf1(
  F);
  a = 0.F or b = 0.F or a is Element of NonZero F & b is Element of
  NonZero F by ZFMISC_1:56;
  hence thesis by Th5;
end;

theorem Th21:
  for F being Field-like Abelian distributive add-associative
  right_zeroed right_complementable non degenerated doubleLoopStr, a being
  Element of F holds a*1.F = a & 1.F*a = a
proof
  let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of suppf1(F);
  per cases by ZFMISC_1:56;
  suppose
A1: a = 0.F;
    hence a*1.F = a;
    thus thesis by A1;
  end;
  suppose
    a is Element of NonZero F;
    hence thesis by Th6;
  end;
end;

definition
  let F be Field;
  func revf(F) -> UnOp of NonZero F means  :Def6:
  for x being Element of NonZero F holds omf(F).(x,it.x) = 1.F;
  existence
  proof
    defpred Z[object,object] means omf(F).($1,$2) = 1.F;
A1: for x being object st x in suppf1(F)\{0.F}
   ex y being object st y in suppf1(F)\{0.F} & Z[x,y]
    proof
      let x be object;
      assume x in suppf1(F)\{0.F};
      then reconsider x as Element of NonZero F;
      consider y being Element of suppf1(F)\{0.F} such that
A2:   x*y = 1.F and
      y*x = 1.F by Th7;
      reconsider y as set;
      take y;
      thus thesis by A2;
    end;
    ex C being Function of suppf1(F)\{0.F},suppf1(F)\{0.F} st for x being
    object st x in suppf1(F)\{0.F} holds Z[x,C.x] from FUNCT_2:sch 1 (A1);
    then consider C being UnOp of NonZero F such that
A3: for x being object st x in suppf1(F)\{0.F} holds omf(F).(x,C.x) = 1.F;
    take C;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let C1,C2 be UnOp of NonZero F such that
A4: for x being Element of NonZero F holds omf(F).(x,C1.x) = 1.F and
A5: for x being Element of NonZero F holds omf(F).(x,C2.x) = 1.F;
    for x being object st x in suppf1(F)\{0.F} holds C1.x = C2.x
    proof
      let x be object;
      assume
A6:   x in suppf1(F)\{0.F};
      then
A7:   C1.x is Element of NonZero F by FUNCT_2:5;
      then reconsider a=x, C1a = C1.x as Element of F by A6;
A8:   C2.x is Element of NonZero F by A6,FUNCT_2:5;
      then reconsider C2a = C2.x as Element of F;
      C1.x = (C1a)*1.F
        .= C1a*(a*C2a) by A5,A6
        .= (a*C1a)*C2a by A6,A7,A8,Th4
        .= 1.F*(C2a) by A4,A6
        .= C2.x;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem
  for F being Field, x,y being Element of NonZero F holds x*y = 1.F
  implies y = revf(F).x
proof
  let F be Field, x,y be Element of NonZero F;
  assume
A1: x*y = 1.F;
  reconsider rx = revf(F).x as Element of F by XBOOLE_0:def 5;
  y = y*1.F
    .= omf(F).(y,1.F)
    .= y*(x*rx) by Def6
    .= 1.F*rx by A1,Th4
    .= revf(F).x;
  hence thesis;
end;

theorem
  for F being Field, x being Element of NonZero F holds x =revf(F).(revf (F).x)
proof
  let F be Field, x be Element of NonZero F;
  reconsider rx = revf(F).x as Element of F by XBOOLE_0:def 5;
  reconsider rrx = revf(F).(revf(F).x) as Element of F by XBOOLE_0:def 5;
  x =x*1.F
    .= omf(F).(x,1.F)
    .= x*(rx*rrx) by Def6
    .= x*rx*rrx by Th4
    .= omf(F).(1.F,revf(F).(revf(F).x)) by Def6
    .= 1.F*rrx
    .= revf(F).(revf(F).x);
  hence thesis;
end;

theorem
  for F being Field, a,b being Element of NonZero F holds
  omf(F).(a,b) is Element of NonZero F & revf(F).a is Element of NonZero F
proof
  let F be Field, a,b be Element of NonZero F;
  [a,b] in [:NonZero F,NonZero F:];
  hence thesis by REALSET1:def 4;
end;

theorem
  for F being Field, a,b,c being Element of F holds a+b = a+c implies
  b = c by RLVECT_1:8;

theorem
  for F being Field, a being Element of NonZero F,
      b,c being Element of F holds a*b = a*c implies b = c
proof
  let F be Field, a be Element of NonZero F, b,c be Element of suppf1(F);
  reconsider x=a as Element of F;
  assume
A1: a*b = a*c;
  reconsider ra = revf(F).a as Element of F by XBOOLE_0:def 5;
  b = 1.F*b
    .= omf(F).(1.F,b)
    .= (x*ra)*b by Def6
    .= ra*(x*c) by A1,Th19
    .= (x*ra)*c by Th19
    .= omf(F).(1.F,c) by Def6
    .= 1.F*c
    .= c;
  hence thesis;
end;

registration
  cluster Field-like Abelian distributive add-associative right_zeroed
    right_complementable -> commutative associative well-unital
    almost_left_invertible for non degenerated doubleLoopStr;
  coherence
  proof
    let L be non degenerated doubleLoopStr;
    assume
A1: L is Field-like Abelian distributive add-associative right_zeroed
    right_complementable;
    then for x,y being Element of L holds x*y = y*x by Th20;
    hence L is commutative by GROUP_1:def 12;
    for x,y,z being Element of L holds (x*y)*z = x*(y*z) by A1,Th19;
    hence L is associative by GROUP_1:def 3;
    for x being Element of L holds x * 1.L = x & 1.L * x = x by A1,Th21;
    hence L is well-unital;
    let x being Element of L;
    assume x <> 0.L;
    then not x in {0.L} by TARSKI:def 1;
    then reconsider x as Element of NonZero L by XBOOLE_0:def 5;
    consider y being Element of NonZero L such that
    x*y = 1.L and
A2: y*x = 1.L by A1,Th7;
    take y;
    thus thesis by A2;
  end;
end;