:: Collective Operations on Number-Membered Sets
::  by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008-2021 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 NUMBERS, SUBSET_1, MEMBERED, XCMPLX_0, XXREAL_0, ARYTM_1,
      RELAT_1, TARSKI, XBOOLE_0, ARYTM_3, RAT_1, INT_1, CARD_1, MEMBER_1,
      NAT_1, REAL_1, XREAL_0, ORDINAL1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, RAT_1, INT_1, MEMBERED, XXREAL_3, XXREAL_0;
 constructors XCMPLX_0, RAT_1, MEMBERED, ENUMSET1, BINOP_2, XXREAL_3;
 registrations XREAL_0, INT_1, RAT_1, ORDINAL1, MEMBERED, XCMPLX_0, NAT_1,
      XXREAL_3, XBOOLE_0;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM;


begin

reserve w, w1, w2 for Element of ExtREAL;
reserve c, c1, c2 for Complex;
reserve A, B, C, D for complex-membered set;
reserve F, G, H, I for ext-real-membered set;
reserve a, b, s, t, z for Complex;
reserve f, g, h, i, j for ExtReal;
reserve r for Real;
reserve e for set;

definition
  let w;
  redefine func -w -> Element of ExtREAL;
  redefine func w" -> Element of ExtREAL;
  let w1;
  redefine func w*w1 -> Element of ExtREAL;
end;

registration
  let a, b, c, d be Complex;
  cluster {a,b,c,d} -> complex-membered;
end;

registration
  let a, b, c, d be ExtReal;
  cluster {a,b,c,d} -> ext-real-membered;
end;

definition
  let F be ext-real-membered set;
  func --F -> ext-real-membered set equals
:: MEMBER_1:def 1
  {-w: w in F};
  involutiveness;
end;

theorem :: MEMBER_1:1
  f in F iff -f in --F;

theorem :: MEMBER_1:2
  -f in F iff f in --F;

registration
  let F be empty set;
  cluster --F -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  cluster --F -> non empty;
end;

theorem :: MEMBER_1:3
  F c= G iff --F c= --G;

theorem :: MEMBER_1:4
  --F = --G implies F = G;

theorem :: MEMBER_1:5
  -- (F \/ G) = (--F) \/ (--G);

theorem :: MEMBER_1:6
  -- (F /\ G) = (--F) /\ (--G);

theorem :: MEMBER_1:7
  -- (F \ G) = (--F) \ (--G);

theorem :: MEMBER_1:8
  -- (F \+\ G) = (--F) \+\ (--G);

theorem :: MEMBER_1:9
  --{f} = {-f};

theorem :: MEMBER_1:10
  --{f,g} = {-f,-g};

definition
  let A be complex-membered set;
  func --A -> complex-membered set equals
:: MEMBER_1:def 2
  {-c: c in A};
  involutiveness;
end;

theorem :: MEMBER_1:11
  a in A iff -a in --A;

theorem :: MEMBER_1:12
  -a in A iff a in --A;

registration
  let A be empty set;
  cluster --A -> empty;
end;

registration
  let A be complex-membered non empty set;
  cluster --A -> non empty;
end;

registration
  let A be real-membered set;
  cluster --A -> real-membered;
end;

registration
  let A be rational-membered set;
  cluster --A -> rational-membered;
end;

registration
  let A be integer-membered set;
  cluster --A -> integer-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  identify --A with --F when A = F;
end;

theorem :: MEMBER_1:13
  A c= B iff --A c= --B;

theorem :: MEMBER_1:14
  --A = --B implies A = B;

theorem :: MEMBER_1:15
  -- (A \/ B) = (--A) \/ (--B);

theorem :: MEMBER_1:16
  -- (A /\ B) = (--A) /\ (--B);

theorem :: MEMBER_1:17
  -- (A \ B) = (--A) \ (--B);

theorem :: MEMBER_1:18
  -- (A \+\ B) = (--A) \+\ (--B);

theorem :: MEMBER_1:19
  --{a} = {-a};

theorem :: MEMBER_1:20
  --{a,b} = {-a,-b};

definition
  let F be ext-real-membered set;
  func F"" -> ext-real-membered set equals
:: MEMBER_1:def 3
  {w": w in F};
end;

theorem :: MEMBER_1:21
  f in F implies f" in F"";

registration
  let F be empty set;
  cluster F"" -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  cluster F"" -> non empty;
end;

theorem :: MEMBER_1:22
  F c= G implies F"" c= G"";

theorem :: MEMBER_1:23
  (F \/ G)"" = (F"") \/ (G"");

theorem :: MEMBER_1:24
  (F /\ G)"" c= (F"") /\ (G"");

theorem :: MEMBER_1:25
  --(F"") = (--F)"";

theorem :: MEMBER_1:26
  {f}"" = {f"};

theorem :: MEMBER_1:27
  {f,g}"" = {f",g"};

definition
  let A be complex-membered set;
  func A"" -> complex-membered set equals
:: MEMBER_1:def 4
  {c": c in A};
  involutiveness;
end;

theorem :: MEMBER_1:28
  a in A iff a" in A"";

theorem :: MEMBER_1:29
  a" in A iff a in A"";

registration
  let A be empty set;
  cluster A"" -> empty;
end;

registration
  let A be complex-membered non empty set;
  cluster A"" -> non empty;
end;

registration
  let A be real-membered set;
  cluster A"" -> real-membered;
end;

registration
  let A be rational-membered set;
  cluster A"" -> rational-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  identify A"" with F"" when A = F;
end;

theorem :: MEMBER_1:30
  A c= B iff A"" c= B"";

theorem :: MEMBER_1:31
  A"" = B"" implies A = B;

theorem :: MEMBER_1:32
  (A \/ B)"" = (A"") \/ (B"");

theorem :: MEMBER_1:33
  (A /\ B)"" = (A"") /\ (B"");

theorem :: MEMBER_1:34
  (A \ B)"" = (A"") \ (B"");

theorem :: MEMBER_1:35
  (A \+\ B)"" = (A"") \+\ (B"");

theorem :: MEMBER_1:36
  --(A"") = (--A)"";

theorem :: MEMBER_1:37
  {a}"" = {a"};

theorem :: MEMBER_1:38
  {a,b}"" = {a",b"};

definition
  let F, G be ext-real-membered set;
  func F++G -> set equals
:: MEMBER_1:def 5
  {w1+w2: w1 in F & w2 in G};
  commutativity;
end;

theorem :: MEMBER_1:39
  f in F & g in G implies f+g in F++G;

registration
  let F be empty set;
  let G be ext-real-membered set;
  cluster F++G -> empty;
  cluster G++F -> empty;
end;

registration
  let F, G be ext-real-membered non empty set;
  cluster F++G -> non empty;
end;

registration
  let F, G be ext-real-membered set;
  cluster F++G -> ext-real-membered;
end;

theorem :: MEMBER_1:40
  F c= G & H c= I implies F++H c= G++I;

theorem :: MEMBER_1:41
  F ++ (G \/ H) = (F++G) \/ (F++H);

theorem :: MEMBER_1:42
  F ++ (G /\ H) c= (F++G) /\ (F++H);

theorem :: MEMBER_1:43
  {f}++{g} = {f+g};

theorem :: MEMBER_1:44
  {f}++{g,h} = {f+g,f+h};

theorem :: MEMBER_1:45
  {f,g}++{h,i} = {f+h,f+i,g+h,g+i};

definition
  let A, B be complex-membered set;
  func A++B -> set equals
:: MEMBER_1:def 6
  {c1+c2: c1 in A & c2 in B};
  commutativity;
end;

theorem :: MEMBER_1:46
  a in A & b in B implies a+b in A++B;

registration
  let A be empty set;
  let B be complex-membered set;
  cluster A++B -> empty;
  cluster B++A -> empty;
end;

registration
  let A, B be complex-membered non empty set;
  cluster A++B -> non empty;
end;

registration
  let A, B be complex-membered set;
  cluster A++B -> complex-membered;
end;

registration
  let A, B be real-membered set;
  cluster A++B -> real-membered;
end;

registration
  let A, B be rational-membered set;
  cluster A++B -> rational-membered;
end;

registration
  let A, B be integer-membered set;
  cluster A++B -> integer-membered;
end;

registration
  let A, B be natural-membered set;
  cluster A++B -> natural-membered;
end;

registration
  let A, B be real-membered set, F, G be ext-real-membered set;
  identify A++B with F++G when A = F, B = G;
end;

theorem :: MEMBER_1:47
  A c= B & C c= D implies A++C c= B++D;

theorem :: MEMBER_1:48
  A ++ (B \/ C) = (A++B) \/ (A++C);

theorem :: MEMBER_1:49
  A ++ (B /\ C) c= (A++B) /\ (A++C);

theorem :: MEMBER_1:50
  (A++B)++C = A++(B++C);

theorem :: MEMBER_1:51
  {a}++{b} = {a+b};

theorem :: MEMBER_1:52
  {a}++{s,t} = {a+s,a+t};

theorem :: MEMBER_1:53
  {a,b}++{s,t} = {a+s,a+t,b+s,b+t};

definition
  let F, G be ext-real-membered set;
  func F--G -> set equals
:: MEMBER_1:def 7
  F ++ --G;
end;

theorem :: MEMBER_1:54
  F--G = {w1-w2: w1 in F & w2 in G};

theorem :: MEMBER_1:55
  f in F & g in G implies f-g in F--G;

registration
  let F be empty set;
  let G be ext-real-membered set;
  cluster F--G -> empty;
  cluster G--F -> empty;
end;

registration
  let F, G be ext-real-membered non empty set;
  cluster F--G -> non empty;
end;

registration
  let F, G be ext-real-membered set;
  cluster F--G -> ext-real-membered;
end;

theorem :: MEMBER_1:56
  F c= G & H c= I implies F--H c= G--I;

theorem :: MEMBER_1:57
  F -- (G \/ H) = (F--G) \/ (F--H);

theorem :: MEMBER_1:58
  F -- (G /\ H) c= (F--G) /\ (F--H);

theorem :: MEMBER_1:59
  --(F++G) = (--F) -- G;

theorem :: MEMBER_1:60
  --(F--G) = (--F) ++ G;

theorem :: MEMBER_1:61
  {f}--{g} = {f-g};

theorem :: MEMBER_1:62
  {f}--{h,i} = {f-h,f-i};

theorem :: MEMBER_1:63
  {f,g}--{h} = {f-h,g-h};

theorem :: MEMBER_1:64
  {f,g}--{h,i} = {f-h,f-i,g-h,g-i};

definition
  let A, B be complex-membered set;
  func A--B -> set equals
:: MEMBER_1:def 8
  A ++ --B;
end;

theorem :: MEMBER_1:65
  A--B = {c1-c2: c1 in A & c2 in B};

theorem :: MEMBER_1:66
  a in A & b in B implies a-b in A--B;

registration
  let A be empty set;
  let B be complex-membered set;
  cluster A--B -> empty;
  cluster B--A -> empty;
end;

registration
  let A, B be complex-membered non empty set;
  cluster A--B -> non empty;
end;

registration
  let A, B be complex-membered set;
  cluster A--B -> complex-membered;
end;

registration
  let A, B be real-membered set;
  cluster A--B -> real-membered;
end;

registration
  let A, B be rational-membered set;
  cluster A--B -> rational-membered;
end;

registration
  let A, B be integer-membered set;
  cluster A--B -> integer-membered;
end;

registration
  let A, B be real-membered set, F, G be ext-real-membered set;
  identify A--B with F--G when A = F, B = G;
end;

theorem :: MEMBER_1:67
  A c= B & C c= D implies A--C c= B--D;

theorem :: MEMBER_1:68
  A -- (B \/ C) = (A--B) \/ (A--C);

theorem :: MEMBER_1:69
  A -- (B /\ C) c= (A--B) /\ (A--C);

theorem :: MEMBER_1:70
  --(A++B) = (--A) -- B;

theorem :: MEMBER_1:71
  --(A--B) = (--A) ++ B;

theorem :: MEMBER_1:72
  A++(B--C) = A++B--C;

theorem :: MEMBER_1:73
  A--(B++C) = A--B--C;

theorem :: MEMBER_1:74
  A--(B--C) = A--B++C;

theorem :: MEMBER_1:75
  {a}--{b} = {a-b};

theorem :: MEMBER_1:76
  {a}--{s,t} = {a-s,a-t};

theorem :: MEMBER_1:77
  {a,b}--{s} = {a-s,b-s};

theorem :: MEMBER_1:78
  {a,b}--{s,t} = {a-s,a-t,b-s,b-t};

definition
  let F, G be ext-real-membered set;
  func F**G -> set equals
:: MEMBER_1:def 9
  {w1*w2: w1 in F & w2 in G};
  commutativity;
end;

registration
  let F be empty set;
  let G be ext-real-membered set;
  cluster F**G -> empty;
  cluster G**F -> empty;
end;

registration
  let F, G be ext-real-membered set;
  cluster F**G -> ext-real-membered;
end;

theorem :: MEMBER_1:79
  f in F & g in G implies f*g in F**G;

registration
  let F, G be ext-real-membered non empty set;
  cluster F**G -> non empty;
end;

theorem :: MEMBER_1:80
  (F**G)**H = F**(G**H);

theorem :: MEMBER_1:81
  F c= G & H c= I implies F**H c= G**I;

theorem :: MEMBER_1:82
  F ** (G \/ H) = (F**G) \/ (F**H);

theorem :: MEMBER_1:83
  F ** (G /\ H) c= (F**G) /\ (F**H);

theorem :: MEMBER_1:84
  F**--G = --(F**G);

theorem :: MEMBER_1:85
  (F**G)"" = (F"") ** (G"");

theorem :: MEMBER_1:86
  {f}**{g} = {f*g};

theorem :: MEMBER_1:87
  {f}**{h,i} = {f*h,f*i};

theorem :: MEMBER_1:88
  {f,g}**{h,i} = {f*h,f*i,g*h,g*i};

definition
  let A, B be complex-membered set;
  func A**B -> set equals
:: MEMBER_1:def 10
  {c1*c2: c1 in A & c2 in B};
  commutativity;
end;

theorem :: MEMBER_1:89
  a in A & b in B implies a*b in A**B;

registration
  let A be empty set;
  let B be complex-membered set;
  cluster A**B -> empty;
  cluster B**A -> empty;
end;

registration
  let A, B be complex-membered non empty set;
  cluster A**B -> non empty;
end;

registration
  let A, B be complex-membered set;
  cluster A**B -> complex-membered;
end;

registration
  let A, B be real-membered set;
  cluster A**B -> real-membered;
end;

registration
  let A, B be rational-membered set;
  cluster A**B -> rational-membered;
end;

registration
  let A, B be integer-membered set;
  cluster A**B -> integer-membered;
end;

registration
  let A, B be natural-membered set;
  cluster A**B -> natural-membered;
end;

registration
  let A, B be real-membered set, F, G be ext-real-membered set;
  identify A**B with F**G when A = F, B = G;
end;

theorem :: MEMBER_1:90
  (A**B)**C = A**(B**C);

theorem :: MEMBER_1:91
  A c= B & C c= D implies A**C c= B**D;

theorem :: MEMBER_1:92
  A ** (B \/ C) = (A**B) \/ (A**C);

theorem :: MEMBER_1:93
  A ** (B /\ C) c= (A**B) /\ (A**C);

theorem :: MEMBER_1:94
  A**--B = --(A**B);

theorem :: MEMBER_1:95
  A**(B++C) c= A**B ++ A**C;

theorem :: MEMBER_1:96
  A**(B--C) c= A**B -- A**C;

theorem :: MEMBER_1:97
  (A**B)"" = (A"") ** (B"");

theorem :: MEMBER_1:98
  {a}**{b} = {a*b};

theorem :: MEMBER_1:99
  {a}**{s,t} = {a*s,a*t};

theorem :: MEMBER_1:100
  {a,b}**{s,t} = {a*s,a*t,b*s,b*t};

definition
  let F, G be ext-real-membered set;
  func F///G -> set equals
:: MEMBER_1:def 11
  F**(G"");
end;

theorem :: MEMBER_1:101
  F///G = {w1/w2: w1 in F & w2 in G};

theorem :: MEMBER_1:102
  f in F & g in G implies f/g in F///G;

registration
  let F be empty set;
  let G be ext-real-membered set;
  cluster F///G -> empty;
  cluster G///F -> empty;
end;

registration
  let F, G be ext-real-membered non empty set;
  cluster F///G -> non empty;
end;

registration
  let F, G be ext-real-membered set;
  cluster F///G -> ext-real-membered;
end;

theorem :: MEMBER_1:103
  F c= G & H c= I implies F///H c= G///I;

theorem :: MEMBER_1:104
  (F \/ G) /// H = (F///H) \/ (G///H);

theorem :: MEMBER_1:105
  (F /\ G) /// H c= (F///H) /\ (G///H);

theorem :: MEMBER_1:106
  F /// (G \/ H) = (F///G) \/ (F///H);

theorem :: MEMBER_1:107
  F /// (G /\ H) c= (F///G) /\ (F///H);

theorem :: MEMBER_1:108
  (F**G)///H = F**(G///H);

theorem :: MEMBER_1:109
  (F///G)**H = (F**H)///G;

theorem :: MEMBER_1:110
  (F///G)///H = F///(G**H);

theorem :: MEMBER_1:111
  {f}///{g} = {f/g};

theorem :: MEMBER_1:112
  {f}///{h,i} = {f/h,f/i};

theorem :: MEMBER_1:113
  {f,g}///{h} = {f/h,g/h};

theorem :: MEMBER_1:114
  {f,g}///{h,i} = {f/h,f/i,g/h,g/i};

definition
  let A, B be complex-membered set;
  func A///B -> set equals
:: MEMBER_1:def 12
  A**(B"");
end;

theorem :: MEMBER_1:115
  A///B = {c1/c2: c1 in A & c2 in B};

theorem :: MEMBER_1:116
  a in A & b in B implies a/b in A///B;

registration
  let A be empty set;
  let B be complex-membered set;
  cluster A///B -> empty;
  cluster B///A -> empty;
end;

registration
  let A, B be complex-membered non empty set;
  cluster A///B -> non empty;
end;

registration
  let A, B be complex-membered set;
  cluster A///B -> complex-membered;
end;

registration
  let A, B be real-membered set;
  cluster A///B -> real-membered;
end;

registration
  let A, B be rational-membered set;
  cluster A///B -> rational-membered;
end;

registration
  let A, B be real-membered set, F, G be ext-real-membered set;
  identify A///B with F///G when A = F, B = G;
end;

theorem :: MEMBER_1:117
  A c= B & C c= D implies A///C c= B///D;

theorem :: MEMBER_1:118
  A /// (B \/ C) = (A///B) \/ (A///C);

theorem :: MEMBER_1:119
  A /// (B /\ C) c= (A///B) /\ (A///C);

theorem :: MEMBER_1:120
  A///--B = --(A///B);

theorem :: MEMBER_1:121
  (--A)///B = --(A///B);

theorem :: MEMBER_1:122
  (A++B)///C c= A///C ++ B///C;

theorem :: MEMBER_1:123
  (A--B)///C c= A///C -- B///C;

theorem :: MEMBER_1:124
  (A**B)///C = A**(B///C);

theorem :: MEMBER_1:125
  (A///B)**C = (A**C)///B;

theorem :: MEMBER_1:126
  (A///B)///C = A///(B**C);

theorem :: MEMBER_1:127
  A///(B///C) = (A**C)///B;

theorem :: MEMBER_1:128
  {a}///{b} = {a/b};

theorem :: MEMBER_1:129
  {a}///{s,t} = {a/s,a/t};

theorem :: MEMBER_1:130
  {a,b}///{s} = {a/s,b/s};

theorem :: MEMBER_1:131
  {a,b}///{s,t} = {a/s,a/t,b/s,b/t};

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func f++F -> set equals
:: MEMBER_1:def 13
  {f}++F;
end;

theorem :: MEMBER_1:132
  g in G implies f+g in f++G;

theorem :: MEMBER_1:133
  f++F = {f+w: w in F};

theorem :: MEMBER_1:134
  e in f++F implies ex w st e = f+w & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster f++F -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster f++F -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster f++F -> ext-real-membered;
end;

theorem :: MEMBER_1:135
  r++F c= r++G implies F c= G;

theorem :: MEMBER_1:136
  r++F = r++G implies F = G;

theorem :: MEMBER_1:137
  r ++ (F /\ G) = (r++F) /\ (r++G);

theorem :: MEMBER_1:138
  (f++F) \ (f++G) c= f ++ (F \ G);

theorem :: MEMBER_1:139
  r ++ (F \ G) = (r++F) \ (r++G);

theorem :: MEMBER_1:140
  r ++ (F \+\ G) = (r++F) \+\ (r++G);

definition
  let A be complex-membered set;
  let a be Complex;
  func a++A -> set equals
:: MEMBER_1:def 14
  {a}++A;
end;

theorem :: MEMBER_1:141
  b in A implies a+b in a++A;

theorem :: MEMBER_1:142
  a++A = {a+c: c in A};

theorem :: MEMBER_1:143
  e in a++A implies ex c st e = a+c & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster a++A -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster a++A -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster a++A -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster a++A -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster a++A -> rational-membered;
end;

registration
  let A be integer-membered set;
  let a be Integer;
  cluster a++A -> integer-membered;
end;

registration
  let A be natural-membered set;
  let a be Nat;
  cluster a++A -> natural-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify a++A with f++F when a = f, A = F;
end;

theorem :: MEMBER_1:144
  A c= B iff a++A c= a++B;

theorem :: MEMBER_1:145
  a++A = a++B implies A = B;

theorem :: MEMBER_1:146
  0++A = A;

theorem :: MEMBER_1:147
  (a+b)++A = a++(b++A);

theorem :: MEMBER_1:148
  a++(A++B) = (a++A)++B;

theorem :: MEMBER_1:149
  a ++ (A /\ B) = (a++A) /\ (a++B);

theorem :: MEMBER_1:150
  a ++ (A \ B) = (a++A) \ (a++B);

theorem :: MEMBER_1:151
  a ++ (A \+\ B) = (a++A) \+\ (a++B);

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func f--F -> set equals
:: MEMBER_1:def 15
  {f}--F;
end;

theorem :: MEMBER_1:152
  g in G implies f-g in f--G;

theorem :: MEMBER_1:153
  f--F = {f-w: w in F};

theorem :: MEMBER_1:154
  e in f--F implies ex w st e = f-w & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster f--F -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster f--F -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster f--F -> ext-real-membered;
end;

theorem :: MEMBER_1:155
  r--F c= r--G implies F c= G;

theorem :: MEMBER_1:156
  r--F = r--G implies F = G;

theorem :: MEMBER_1:157
  r -- (F/\G) = (r--F) /\ (r--G);

theorem :: MEMBER_1:158
  r -- (F\G) = (r--F) \ (r--G);

theorem :: MEMBER_1:159
  r -- (F\+\G) = (r--F) \+\ (r--G);

definition
  let A be complex-membered set;
  let a be Complex;
  func a--A -> set equals
:: MEMBER_1:def 16
  {a}--A;
end;

theorem :: MEMBER_1:160
  b in A implies a-b in a--A;

theorem :: MEMBER_1:161
  a--A = {a-c: c in A};

theorem :: MEMBER_1:162
  e in a--A implies ex c st e = a-c & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster a--A -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster a--A -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster a--A -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster a--A -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster a--A -> rational-membered;
end;

registration
  let A be integer-membered set;
  let a be Integer;
  cluster a--A -> integer-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify a--A with f--F when a = f, A = F;
end;

theorem :: MEMBER_1:163
  A c= B iff a--A c= a--B;

theorem :: MEMBER_1:164
  a--A = a--B implies A = B;

theorem :: MEMBER_1:165
  a -- (A/\B) = (a--A) /\ (a--B);

theorem :: MEMBER_1:166
  a -- (A\B) = (a--A) \ (a--B);

theorem :: MEMBER_1:167
  a -- (A\+\B) = (a--A) \+\ (a--B);

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func F--f -> set equals
:: MEMBER_1:def 17
  F--{f};
end;

theorem :: MEMBER_1:168
  g in G implies g-f in G--f;

theorem :: MEMBER_1:169
  F--f = {w-f: w in F};

theorem :: MEMBER_1:170
  e in F--f implies ex w st e = w-f & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster F--f -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster F--f -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster F--f -> ext-real-membered;
end;

theorem :: MEMBER_1:171
  F -- f = -- (f -- F);

theorem :: MEMBER_1:172
  f -- F = -- (F -- f);

theorem :: MEMBER_1:173
  (F/\G) -- r = (F--r) /\ (G--r);

theorem :: MEMBER_1:174
  (F\G) -- r = (F--r) \ (G--r);

theorem :: MEMBER_1:175
  (F\+\G) -- r = (F--r) \+\ (G--r);

definition
  let A be complex-membered set;
  let a be Complex;
  func A--a -> set equals
:: MEMBER_1:def 18
  A--{a};
end;

theorem :: MEMBER_1:176
  b in A implies b-a in A--a;

theorem :: MEMBER_1:177
  A--a = {c-a: c in A};

theorem :: MEMBER_1:178
  e in A--a implies ex c st e = c-a & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster A--a -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster A--a -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster A--a -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster A--a -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster A--a -> rational-membered;
end;

registration
  let A be integer-membered set;
  let a be Integer;
  cluster A--a -> integer-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify A--a with F--f when a = f, A = F;
end;

theorem :: MEMBER_1:179
  A c= B iff A--a c= B--a;

theorem :: MEMBER_1:180
  A--a = B--a implies A = B;

theorem :: MEMBER_1:181
  A -- a = -- (a -- A);

theorem :: MEMBER_1:182
  a -- A = -- (A -- a);

theorem :: MEMBER_1:183
  (A/\B) -- a = (A--a) /\ (B--a);

theorem :: MEMBER_1:184
  (A\B) -- a = (A--a) \ (B--a);

theorem :: MEMBER_1:185
  (A\+\B) -- a = (A--a) \+\ (B--a);

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func f**F -> set equals
:: MEMBER_1:def 19
  {f}**F;
end;

theorem :: MEMBER_1:186
  g in G implies f*g in f**G;

theorem :: MEMBER_1:187
  f**F = {f*w: w in F};

theorem :: MEMBER_1:188
  e in f**F implies ex w st e = f*w & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster f**F -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster f**F -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster f**F -> ext-real-membered;
end;

theorem :: MEMBER_1:189
  r <> 0 implies r ** (F/\G) = (r**F) /\ (r**G);

theorem :: MEMBER_1:190
  (f**F) \ (f**G) c= f ** (F \ G);

theorem :: MEMBER_1:191
  r <> 0 implies r ** (F\G) = (r**F) \ (r**G);

theorem :: MEMBER_1:192
  r <> 0 implies r ** (F\+\G) = (r**F) \+\ (r**G);

definition
  let A be complex-membered set;
  let a be Complex;
  func a**A -> set equals
:: MEMBER_1:def 20
  {a}**A;
end;

theorem :: MEMBER_1:193
  b in A implies a*b in a**A;

theorem :: MEMBER_1:194
  a**A = {a*c: c in A};

theorem :: MEMBER_1:195
  e in a**A implies ex c st e = a*c & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster a**A -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster a**A -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster a**A -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster a**A -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster a**A -> rational-membered;
end;

registration
  let A be integer-membered set;
  let a be Integer;
  cluster a**A -> integer-membered;
end;

registration
  let A be natural-membered set;
  let a be Nat;
  cluster a**A -> natural-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify a**A with f**F when a = f, A = F;
end;

theorem :: MEMBER_1:196
  a <> 0 & a**A c= a**B implies A c= B;

theorem :: MEMBER_1:197
  a <> 0 & a**A = a**B implies A = B;

theorem :: MEMBER_1:198
  a <> 0 implies a ** (A/\B) = (a**A) /\ (a**B);

theorem :: MEMBER_1:199
  a <> 0 implies a ** (A\B) = (a**A) \ (a**B);

theorem :: MEMBER_1:200
  a <> 0 implies a ** (A\+\B) = (a**A) \+\ (a**B);

theorem :: MEMBER_1:201
  0**A c= {0};

theorem :: MEMBER_1:202
  A <> {} implies 0**A = {0};

theorem :: MEMBER_1:203
  1**A = A;

theorem :: MEMBER_1:204
  (a*b)**A = a**(b**A);

theorem :: MEMBER_1:205
  a**(A**B) = (a**A)**B;

theorem :: MEMBER_1:206
  (a+b)**A c= a**A ++ b**A;

theorem :: MEMBER_1:207
  (a-b)**A c= a**A -- b**A;

theorem :: MEMBER_1:208
  a**(B++C) = a**B++a**C;

theorem :: MEMBER_1:209
  a**(B--C) = a**B--a**C;

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func f///F -> set equals
:: MEMBER_1:def 21
  {f}///F;
end;

theorem :: MEMBER_1:210
  g in G implies f/g in f///G;

theorem :: MEMBER_1:211
  f///F = {f/w: w in F};

theorem :: MEMBER_1:212
  e in f///F implies ex w st e = f/w & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster f///F -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster f///F -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster f///F -> ext-real-membered;
end;

definition
  let A be complex-membered set;
  let a be Complex;
  func a///A -> set equals
:: MEMBER_1:def 22
  {a}///A;
end;

theorem :: MEMBER_1:213
  b in A implies a/b in a///A;

theorem :: MEMBER_1:214
  a///A = {a/c: c in A};

theorem :: MEMBER_1:215
  e in a///A implies ex c st e = a/c & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster a///A -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster a///A -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster a///A -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster a///A -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster a///A -> rational-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify a///A with f///F when a = f, A = F;
end;

theorem :: MEMBER_1:216
  a <> 0 & a///A c= a///B implies A c= B;

theorem :: MEMBER_1:217
  a <> 0 & a///A = a///B implies A = B;

theorem :: MEMBER_1:218
  a <> 0 implies a /// (A/\B) = (a///A) /\ (a///B);

theorem :: MEMBER_1:219
  a <> 0 implies a /// (A\B) = (a///A) \ (a///B);

theorem :: MEMBER_1:220
  a <> 0 implies a /// (A\+\B) = (a///A) \+\ (a///B);

theorem :: MEMBER_1:221
  (a+b)///A c= a///A ++ b///A;

theorem :: MEMBER_1:222
  (a-b)///A c= a///A -- b///A;

definition
  let F be ext-real-membered set;
  let f be ExtReal;
  func F///f -> set equals
:: MEMBER_1:def 23
  F///{f};
end;

theorem :: MEMBER_1:223
  g in G implies g/f in G///f;

theorem :: MEMBER_1:224
  F///f = {w/f: w in F};

theorem :: MEMBER_1:225
  e in F///f implies ex w st e = w/f & w in F;

registration
  let F be empty set;
  let f be ExtReal;
  cluster F///f -> empty;
end;

registration
  let F be ext-real-membered non empty set;
  let f be ExtReal;
  cluster F///f -> non empty;
end;

registration
  let F be ext-real-membered set;
  let f be ExtReal;
  cluster F///f -> ext-real-membered;
end;

definition
  let A be complex-membered set;
  let a be Complex;
  func A///a -> set equals
:: MEMBER_1:def 24
  A///{a};
end;

theorem :: MEMBER_1:226
  b in A implies b/a in A///a;

theorem :: MEMBER_1:227
  A///a = {c/a: c in A};

theorem :: MEMBER_1:228
  e in A///a implies ex c st e = c/a & c in A;

registration
  let A be empty set;
  let a be Complex;
  cluster A///a -> empty;
end;

registration
  let A be complex-membered non empty set;
  let a be Complex;
  cluster A///a -> non empty;
end;

registration
  let A be complex-membered set;
  let a be Complex;
  cluster A///a -> complex-membered;
end;

registration
  let A be real-membered set;
  let a be Real;
  cluster A///a -> real-membered;
end;

registration
  let A be rational-membered set;
  let a be Rational;
  cluster A///a -> rational-membered;
end;

registration
  let A be real-membered set, F be ext-real-membered set;
  let a be Real, f be ExtReal;
  identify A///a with F///f when a = f, A = F;
end;

theorem :: MEMBER_1:229
  a <> 0 & A///a c= B///a implies A c= B;

theorem :: MEMBER_1:230
  a <> 0 & A///a = B///a implies A = B;

theorem :: MEMBER_1:231
  a <> 0 implies (A/\B) /// a = (A///a) /\ (B///a);

theorem :: MEMBER_1:232
  a <> 0 implies (A\B) /// a = (A///a) \ (B///a);

theorem :: MEMBER_1:233
  a <> 0 implies (A\+\B) /// a = (A///a) \+\ (B///a);

theorem :: MEMBER_1:234
  (A++B)///a = A///a ++ B///a;

theorem :: MEMBER_1:235
  (A--B)///a = A///a -- B///a;