:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let w be Element of ExtREAL ;
:: original:-
redefine func - w ->  Element of ExtREAL ;
coherence
 - w is Element of ExtREAL by XXREAL_0:def_1;
:: original:"
redefine funcw "  ->  Element of ExtREAL ;
coherence
 w " is Element of ExtREAL by XXREAL_0:def_1;
let w1 be Element of ExtREAL ;
:: original:*
redefine funcw * w1 ->  Element of ExtREAL ;
coherence
 w * w1 is Element of ExtREAL by XXREAL_0:def_1;
end;

registration
let a, b, c, d be complex number ;
cluster{a,b,c,d} ->  complex-membered ;
coherence
 {a,b,c,d} is complex-membered
proofend;
end;

registration
let a, b, c, d be ext-real number ;
cluster{a,b,c,d} ->  ext-real-membered ;
coherence
 {a,b,c,d} is ext-real-membered
proofend;
end;

definition
let F be ext-real-membered set ;
func -- F ->  ext-real-membered set  equals :: MEMBER_1:def 1
 {  (- w) where w is Element of ExtREAL : w in F  }  ;
coherence
  {  (- w) where w is Element of ExtREAL : w in F  }  is ext-real-membered set
proofend;
involutiveness
 for b1, b2 being ext-real-membered set st b1 =  {  (- w) where w is Element of ExtREAL : w in b2  }  holds
b2 =  {  (- w) where w is Element of ExtREAL : w in b1  }
proofend;
end;

:: deftheorem  defines -- MEMBER_1:def_1_:_
 for F being ext-real-membered set holds -- F =  {  (- w) where w is Element of ExtREAL : w in F  }  ;

theorem Th1: :: MEMBER_1:1
for F being ext-real-membered set
for f being ext-real number holds
( f in F iff - f in -- F )
proofend;

theorem Th2: :: MEMBER_1:2
for F being ext-real-membered set
for f being ext-real number holds
( - f in F iff f in -- F )
proofend;

registration
let F be empty set ;
cluster -- F ->  empty ext-real-membered ;
coherence
 -- F is empty
proofend;
end;

registration
let F be non empty ext-real-membered set ;
cluster -- F ->  non empty ext-real-membered ;
coherence
 not -- F is empty
proofend;
end;

Lm1:  for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
proofend;

theorem Th3: :: MEMBER_1:3
for F, G being ext-real-membered set holds
( F c= G iff -- F c= -- G )
proofend;

theorem :: MEMBER_1:4
for F, G being ext-real-membered set st -- F = -- G holds
F = G
proofend;

theorem Th5: :: MEMBER_1:5
for F, G being ext-real-membered set holds -- (F \/ G) = (-- F) \/ (-- G)
proofend;

theorem Th6: :: MEMBER_1:6
for F, G being ext-real-membered set holds -- (F /\ G) = (-- F) /\ (-- G)
proofend;

theorem Th7: :: MEMBER_1:7
for F, G being ext-real-membered set holds -- (F \ G) = (-- F) \ (-- G)
proofend;

theorem Th8: :: MEMBER_1:8
for F, G being ext-real-membered set holds -- (F \+\ G) = (-- F) \+\ (-- G)
proofend;

theorem Th9: :: MEMBER_1:9
for f being ext-real number holds -- {f} = {(- f)}
proofend;

theorem Th10: :: MEMBER_1:10
for f, g being ext-real number holds -- {f,g} = {(- f),(- g)}
proofend;

definition
let A be complex-membered set ;
func -- A ->  complex-membered set  equals :: MEMBER_1:def 2
 {  (- c) where c is Element of COMPLEX : c in A  }  ;
coherence
  {  (- c) where c is Element of COMPLEX : c in A  }  is complex-membered set
proofend;
involutiveness
 for b1, b2 being complex-membered set st b1 =  {  (- c) where c is Element of COMPLEX : c in b2  }  holds
b2 =  {  (- c) where c is Element of COMPLEX : c in b1  }
proofend;
end;

:: deftheorem  defines -- MEMBER_1:def_2_:_
 for A being complex-membered set holds -- A =  {  (- c) where c is Element of COMPLEX : c in A  }  ;

theorem Th11: :: MEMBER_1:11
for A being complex-membered set
for a being complex number holds
( a in A iff - a in -- A )
proofend;

theorem Th12: :: MEMBER_1:12
for A being complex-membered set
for a being complex number holds
( - a in A iff a in -- A )
proofend;

registration
let A be empty set ;
cluster -- A ->  empty complex-membered ;
coherence
 -- A is empty
proofend;
end;

registration
let A be non empty complex-membered set ;
cluster -- A ->  non empty complex-membered ;
coherence
 not -- A is empty
proofend;
end;

registration
let A be real-membered set ;
cluster -- A ->  complex-membered real-membered ;
coherence
 -- A is real-membered
proofend;
end;

registration
let A be rational-membered set ;
cluster -- A ->  complex-membered rational-membered ;
coherence
 -- A is rational-membered
proofend;
end;

registration
let A be integer-membered set ;
cluster -- A ->  complex-membered integer-membered ;
coherence
 -- A is integer-membered
proofend;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
identify -- A with  -- F when A = F;
compatibility
 ( A = F implies -- A = -- F )
proofend;
end;

Lm2:  for A, B being complex-membered set st A c= B holds
-- A c= -- B
proofend;

theorem Th13: :: MEMBER_1:13
for A, B being complex-membered set holds
( A c= B iff -- A c= -- B )
proofend;

theorem :: MEMBER_1:14
for A, B being complex-membered set st -- A = -- B holds
A = B
proofend;

theorem Th15: :: MEMBER_1:15
for A, B being complex-membered set holds -- (A \/ B) = (-- A) \/ (-- B)
proofend;

theorem Th16: :: MEMBER_1:16
for A, B being complex-membered set holds -- (A /\ B) = (-- A) /\ (-- B)
proofend;

theorem Th17: :: MEMBER_1:17
for A, B being complex-membered set holds -- (A \ B) = (-- A) \ (-- B)
proofend;

theorem Th18: :: MEMBER_1:18
for A, B being complex-membered set holds -- (A \+\ B) = (-- A) \+\ (-- B)
proofend;

theorem Th19: :: MEMBER_1:19
for a being complex number holds -- {a} = {(- a)}
proofend;

theorem Th20: :: MEMBER_1:20
for a, b being complex number holds -- {a,b} = {(- a),(- b)}
proofend;

definition
let F be ext-real-membered set ;
funcF ""  ->  ext-real-membered set  equals :: MEMBER_1:def 3
 {  (w ") where w is Element of ExtREAL : w in F  }  ;
coherence
  {  (w ") where w is Element of ExtREAL : w in F  }  is ext-real-membered set
proofend;
end;

:: deftheorem  defines "" MEMBER_1:def_3_:_
 for F being ext-real-membered set holds F "" =  {  (w ") where w is Element of ExtREAL : w in F  }  ;

theorem Th21: :: MEMBER_1:21
for F being ext-real-membered set
for f being ext-real number st f in F holds
f " in F ""
proofend;

registration
let F be empty set ;
clusterF ""  ->  empty ext-real-membered ;
coherence
 F "" is empty
proofend;
end;

registration
let F be non empty ext-real-membered set ;
clusterF ""  ->  non empty ext-real-membered ;
coherence
 not F "" is empty
proofend;
end;

theorem :: MEMBER_1:22
for F, G being ext-real-membered set st F c= G holds
F "" c= G ""
proofend;

theorem Th23: :: MEMBER_1:23
for F, G being ext-real-membered set holds (F \/ G) "" = (F "") \/ (G "")
proofend;

theorem Th24: :: MEMBER_1:24
for F, G being ext-real-membered set holds (F /\ G) "" c= (F "") /\ (G "")
proofend;

theorem :: MEMBER_1:25
for F being ext-real-membered set holds -- (F "") = (-- F) ""
proofend;

theorem Th26: :: MEMBER_1:26
for f being ext-real number holds {f} "" = {(f ")}
proofend;

theorem Th27: :: MEMBER_1:27
for f, g being ext-real number holds {f,g} "" = {(f "),(g ")}
proofend;

definition
let A be complex-membered set ;
funcA ""  ->  complex-membered set  equals :: MEMBER_1:def 4
 {  (c ") where c is Element of COMPLEX : c in A  }  ;
coherence
  {  (c ") where c is Element of COMPLEX : c in A  }  is complex-membered set
proofend;
involutiveness
 for b1, b2 being complex-membered set st b1 =  {  (c ") where c is Element of COMPLEX : c in b2  }  holds
b2 =  {  (c ") where c is Element of COMPLEX : c in b1  }
proofend;
end;

:: deftheorem  defines "" MEMBER_1:def_4_:_
 for A being complex-membered set holds A "" =  {  (c ") where c is Element of COMPLEX : c in A  }  ;

theorem Th28: :: MEMBER_1:28
for A being complex-membered set
for a being complex number holds
( a in A iff a " in A "" )
proofend;

theorem Th29: :: MEMBER_1:29
for A being complex-membered set
for a being complex number holds
( a " in A iff a in A "" )
proofend;

registration
let A be empty set ;
clusterA ""  ->  empty complex-membered ;
coherence
 A "" is empty
proofend;
end;

registration
let A be non empty complex-membered set ;
clusterA ""  ->  non empty complex-membered ;
coherence
 not A "" is empty
proofend;
end;

registration
let A be real-membered set ;
clusterA ""  ->  complex-membered real-membered ;
coherence
 A "" is real-membered
proofend;
end;

registration
let A be rational-membered set ;
clusterA ""  ->  complex-membered rational-membered ;
coherence
 A "" is rational-membered
proofend;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
identifyA ""  with F ""  when A = F;
compatibility
 ( A = F implies A "" = F "" )
proofend;
end;

Lm3:  for A, B being complex-membered set st A c= B holds
A "" c= B ""
proofend;

theorem Th30: :: MEMBER_1:30
for A, B being complex-membered set holds
( A c= B iff A "" c= B "" )
proofend;

theorem :: MEMBER_1:31
for A, B being complex-membered set st A "" = B "" holds
A = B
proofend;

theorem Th32: :: MEMBER_1:32
for A, B being complex-membered set holds (A \/ B) "" = (A "") \/ (B "")
proofend;

theorem Th33: :: MEMBER_1:33
for A, B being complex-membered set holds (A /\ B) "" = (A "") /\ (B "")
proofend;

theorem Th34: :: MEMBER_1:34
for A, B being complex-membered set holds (A \ B) "" = (A "") \ (B "")
proofend;

theorem Th35: :: MEMBER_1:35
for A, B being complex-membered set holds (A \+\ B) "" = (A "") \+\ (B "")
proofend;

theorem Th36: :: MEMBER_1:36
for A being complex-membered set holds -- (A "") = (-- A) ""
proofend;

theorem Th37: :: MEMBER_1:37
for a being complex number holds {a} "" = {(a ")}
proofend;

theorem Th38: :: MEMBER_1:38
for a, b being complex number holds {a,b} "" = {(a "),(b ")}
proofend;

definition
let F, G be ext-real-membered set ;
funcF ++ G ->  set  equals :: MEMBER_1:def 5
 {  (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  ;
coherence
  {  (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  is set ;
commutativity
 for b1 being set
for F, G being ext-real-membered set st b1 =  {  (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  holds
b1 =  {  (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F )  }
proofend;
end;

:: deftheorem  defines ++ MEMBER_1:def_5_:_
 for F, G being ext-real-membered set holds F ++ G =  {  (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  ;

theorem Th39: :: MEMBER_1:39
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f + g in F ++ G
proofend;

registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF ++ G ->  empty ;
coherence
 F ++ G is empty
proofend;
clusterG ++ F ->  empty ;
coherence
 G ++ F is empty ;
end;

registration
let F, G be non empty ext-real-membered set ;
clusterF ++ G ->  non empty ;
coherence
 not F ++ G is empty
proofend;
end;

registration
let F, G be ext-real-membered set ;
clusterF ++ G ->  ext-real-membered ;
coherence
 F ++ G is ext-real-membered
proofend;
end;

theorem :: MEMBER_1:40
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F ++ H c= G ++ I
proofend;

theorem Th41: :: MEMBER_1:41
for F, G, H being ext-real-membered set holds F ++ (G \/ H) = (F ++ G) \/ (F ++ H)
proofend;

theorem Th42: :: MEMBER_1:42
for F, G, H being ext-real-membered set holds F ++ (G /\ H) c= (F ++ G) /\ (F ++ H)
proofend;

theorem Th43: :: MEMBER_1:43
for f, g being ext-real number holds {f} ++ {g} = {(f + g)}
proofend;

theorem Th44: :: MEMBER_1:44
for f, g, h being ext-real number holds {f} ++ {g,h} = {(f + g),(f + h)}
proofend;

theorem Th45: :: MEMBER_1:45
for f, g, h, i being ext-real number holds {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)}
proofend;

definition
let A, B be complex-membered set ;
funcA ++ B ->  set  equals :: MEMBER_1:def 6
 {  (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  ;
coherence
  {  (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  is set ;
commutativity
 for b1 being set
for A, B being complex-membered set st b1 =  {  (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  holds
b1 =  {  (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A )  }
proofend;
end;

:: deftheorem  defines ++ MEMBER_1:def_6_:_
 for A, B being complex-membered set holds A ++ B =  {  (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  ;

theorem Th46: :: MEMBER_1:46
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a + b in A ++ B
proofend;

registration
let A be empty set ;
let B be complex-membered set ;
clusterA ++ B ->  empty ;
coherence
 A ++ B is empty
proofend;
clusterB ++ A ->  empty ;
coherence
 B ++ A is empty ;
end;

registration
let A, B be non empty complex-membered set ;
clusterA ++ B ->  non empty ;
coherence
 not A ++ B is empty
proofend;
end;

registration
let A, B be complex-membered set ;
clusterA ++ B ->  complex-membered ;
coherence
 A ++ B is complex-membered
proofend;
end;

registration
let A, B be real-membered set ;
clusterA ++ B ->  real-membered ;
coherence
 A ++ B is real-membered
proofend;
end;

registration
let A, B be rational-membered set ;
clusterA ++ B ->  rational-membered ;
coherence
 A ++ B is rational-membered
proofend;
end;

registration
let A, B be integer-membered set ;
clusterA ++ B ->  integer-membered ;
coherence
 A ++ B is integer-membered
proofend;
end;

registration
let A, B be natural-membered set ;
clusterA ++ B ->  natural-membered ;
coherence
 A ++ B is natural-membered
proofend;
end;

registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA ++ B with F ++ G when A = F, B = G;
compatibility
 ( A = F & B = G implies A ++ B = F ++ G )
proofend;
end;

theorem Th47: :: MEMBER_1:47
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A ++ C c= B ++ D
proofend;

theorem Th48: :: MEMBER_1:48
for A, B, C being complex-membered set holds A ++ (B \/ C) = (A ++ B) \/ (A ++ C)
proofend;

theorem Th49: :: MEMBER_1:49
for A, B, C being complex-membered set holds A ++ (B /\ C) c= (A ++ B) /\ (A ++ C)
proofend;

theorem Th50: :: MEMBER_1:50
for A, B, C being complex-membered set holds (A ++ B) ++ C = A ++ (B ++ C)
proofend;

theorem Th51: :: MEMBER_1:51
for a, b being complex number holds {a} ++ {b} = {(a + b)}
proofend;

theorem Th52: :: MEMBER_1:52
for a, s, t being complex number holds {a} ++ {s,t} = {(a + s),(a + t)}
proofend;

theorem Th53: :: MEMBER_1:53
for a, b, s, t being complex number holds {a,b} ++ {s,t} = {(a + s),(a + t),(b + s),(b + t)}
proofend;

definition
let F, G be ext-real-membered set ;
funcF -- G ->  set  equals :: MEMBER_1:def 7
F ++ (-- G);
coherence
 F ++ (-- G) is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_7_:_
 for F, G being ext-real-membered set holds F -- G = F ++ (-- G);

theorem Th54: :: MEMBER_1:54
for F, G being ext-real-membered set holds F -- G =  {  (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }
proofend;

theorem Th55: :: MEMBER_1:55
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f - g in F -- G
proofend;

registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF -- G ->  empty ;
coherence
 F -- G is empty ;
clusterG -- F ->  empty ;
coherence
 G -- F is empty ;
end;

registration
let F, G be non empty ext-real-membered set ;
clusterF -- G ->  non empty ;
coherence
 not F -- G is empty ;
end;

registration
let F, G be ext-real-membered set ;
clusterF -- G ->  ext-real-membered ;
coherence
 F -- G is ext-real-membered ;
end;

theorem :: MEMBER_1:56
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F -- H c= G -- I
proofend;

theorem :: MEMBER_1:57
for F, G, H being ext-real-membered set holds F -- (G \/ H) = (F -- G) \/ (F -- H)
proofend;

theorem :: MEMBER_1:58
for F, G, H being ext-real-membered set holds F -- (G /\ H) c= (F -- G) /\ (F -- H)
proofend;

Lm4:  for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
proofend;

theorem :: MEMBER_1:59
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) -- G by Lm4;

theorem Th60: :: MEMBER_1:60
for F, G being ext-real-membered set holds -- (F -- G) = (-- F) ++ G
proofend;

theorem :: MEMBER_1:61
for f, g being ext-real number holds {f} -- {g} = {(f - g)}
proofend;

theorem :: MEMBER_1:62
for f, h, i being ext-real number holds {f} -- {h,i} = {(f - h),(f - i)}
proofend;

theorem :: MEMBER_1:63
for f, g, h being ext-real number holds {f,g} -- {h} = {(f - h),(g - h)}
proofend;

theorem :: MEMBER_1:64
for f, g, h, i being ext-real number holds {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)}
proofend;

definition
let A, B be complex-membered set ;
funcA -- B ->  set  equals :: MEMBER_1:def 8
A ++ (-- B);
coherence
 A ++ (-- B) is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_8_:_
 for A, B being complex-membered set holds A -- B = A ++ (-- B);

theorem Th65: :: MEMBER_1:65
for A, B being complex-membered set holds A -- B =  {  (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }
proofend;

theorem Th66: :: MEMBER_1:66
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a - b in A -- B
proofend;

registration
let A be empty set ;
let B be complex-membered set ;
clusterA -- B ->  empty ;
coherence
 A -- B is empty ;
clusterB -- A ->  empty ;
coherence
 B -- A is empty ;
end;

registration
let A, B be non empty complex-membered set ;
clusterA -- B ->  non empty ;
coherence
 not A -- B is empty ;
end;

registration
let A, B be complex-membered set ;
clusterA -- B ->  complex-membered ;
coherence
 A -- B is complex-membered ;
end;

registration
let A, B be real-membered set ;
clusterA -- B ->  real-membered ;
coherence
 A -- B is real-membered ;
end;

registration
let A, B be rational-membered set ;
clusterA -- B ->  rational-membered ;
coherence
 A -- B is rational-membered ;
end;

registration
let A, B be integer-membered set ;
clusterA -- B ->  integer-membered ;
coherence
 A -- B is integer-membered ;
end;

registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA -- B with F -- G when A = F, B = G;
compatibility
 ( A = F & B = G implies A -- B = F -- G ) ;
end;

theorem Th67: :: MEMBER_1:67
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A -- C c= B -- D
proofend;

Lm5:  for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)
proofend;

theorem :: MEMBER_1:68
for A, B, C being complex-membered set holds A -- (B \/ C) = (A -- B) \/ (A -- C)
proofend;

theorem :: MEMBER_1:69
for A, B, C being complex-membered set holds A -- (B /\ C) c= (A -- B) /\ (A -- C)
proofend;

theorem :: MEMBER_1:70
for A, B being complex-membered set holds -- (A ++ B) = (-- A) -- B by Lm5;

theorem Th71: :: MEMBER_1:71
for A, B being complex-membered set holds -- (A -- B) = (-- A) ++ B
proofend;

theorem :: MEMBER_1:72
for A, B, C being complex-membered set holds A ++ (B -- C) = (A ++ B) -- C by Th50;

theorem :: MEMBER_1:73
for A, B, C being complex-membered set holds A -- (B ++ C) = (A -- B) -- C
proofend;

theorem :: MEMBER_1:74
for A, B, C being complex-membered set holds A -- (B -- C) = (A -- B) ++ C
proofend;

theorem Th75: :: MEMBER_1:75
for a, b being complex number holds {a} -- {b} = {(a - b)}
proofend;

theorem :: MEMBER_1:76
for a, s, t being complex number holds {a} -- {s,t} = {(a - s),(a - t)}
proofend;

theorem :: MEMBER_1:77
for a, b, s being complex number holds {a,b} -- {s} = {(a - s),(b - s)}
proofend;

theorem :: MEMBER_1:78
for a, b, s, t being complex number holds {a,b} -- {s,t} = {(a - s),(a - t),(b - s),(b - t)}
proofend;

definition
let F, G be ext-real-membered set ;
funcF ** G ->  set  equals :: MEMBER_1:def 9
 {  (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  ;
coherence
  {  (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  is set ;
commutativity
 for b1 being set
for F, G being ext-real-membered set st b1 =  {  (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  holds
b1 =  {  (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F )  }
proofend;
end;

:: deftheorem  defines ** MEMBER_1:def_9_:_
 for F, G being ext-real-membered set holds F ** G =  {  (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }  ;

registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF ** G ->  empty ;
coherence
 F ** G is empty
proofend;
clusterG ** F ->  empty ;
coherence
 G ** F is empty ;
end;

registration
let F, G be ext-real-membered set ;
clusterF ** G ->  ext-real-membered ;
coherence
 F ** G is ext-real-membered
proofend;
end;

theorem Th79: :: MEMBER_1:79
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f * g in F ** G
proofend;

registration
let F, G be non empty ext-real-membered set ;
clusterF ** G ->  non empty ;
coherence
 not F ** G is empty
proofend;
end;

theorem Th80: :: MEMBER_1:80
for F, G, H being ext-real-membered set holds (F ** G) ** H = F ** (G ** H)
proofend;

theorem Th81: :: MEMBER_1:81
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F ** H c= G ** I
proofend;

theorem Th82: :: MEMBER_1:82
for F, G, H being ext-real-membered set holds F ** (G \/ H) = (F ** G) \/ (F ** H)
proofend;

theorem Th83: :: MEMBER_1:83
for F, G, H being ext-real-membered set holds F ** (G /\ H) c= (F ** G) /\ (F ** H)
proofend;

theorem :: MEMBER_1:84
for F, G being ext-real-membered set holds F ** (-- G) = -- (F ** G)
proofend;

theorem Th85: :: MEMBER_1:85
for F, G being ext-real-membered set holds (F ** G) "" = (F "") ** (G "")
proofend;

theorem Th86: :: MEMBER_1:86
for f, g being ext-real number holds {f} ** {g} = {(f * g)}
proofend;

theorem Th87: :: MEMBER_1:87
for f, h, i being ext-real number holds {f} ** {h,i} = {(f * h),(f * i)}
proofend;

theorem Th88: :: MEMBER_1:88
for f, g, h, i being ext-real number holds {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)}
proofend;

definition
let A, B be complex-membered set ;
funcA ** B ->  set  equals :: MEMBER_1:def 10
 {  (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  ;
coherence
  {  (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  is set ;
commutativity
 for b1 being set
for A, B being complex-membered set st b1 =  {  (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  holds
b1 =  {  (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A )  }
proofend;
end;

:: deftheorem  defines ** MEMBER_1:def_10_:_
 for A, B being complex-membered set holds A ** B =  {  (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }  ;

theorem Th89: :: MEMBER_1:89
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a * b in A ** B
proofend;

registration
let A be empty set ;
let B be complex-membered set ;
clusterA ** B ->  empty ;
coherence
 A ** B is empty
proofend;
clusterB ** A ->  empty ;
coherence
 B ** A is empty ;
end;

registration
let A, B be non empty complex-membered set ;
clusterA ** B ->  non empty ;
coherence
 not A ** B is empty
proofend;
end;

registration
let A, B be complex-membered set ;
clusterA ** B ->  complex-membered ;
coherence
 A ** B is complex-membered
proofend;
end;

registration
let A, B be real-membered set ;
clusterA ** B ->  real-membered ;
coherence
 A ** B is real-membered
proofend;
end;

registration
let A, B be rational-membered set ;
clusterA ** B ->  rational-membered ;
coherence
 A ** B is rational-membered
proofend;
end;

registration
let A, B be integer-membered set ;
clusterA ** B ->  integer-membered ;
coherence
 A ** B is integer-membered
proofend;
end;

registration
let A, B be natural-membered set ;
clusterA ** B ->  natural-membered ;
coherence
 A ** B is natural-membered
proofend;
end;

registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA ** B with F ** G when A = F, B = G;
compatibility
 ( A = F & B = G implies A ** B = F ** G )
proofend;
end;

theorem Th90: :: MEMBER_1:90
for A, B, C being complex-membered set holds (A ** B) ** C = A ** (B ** C)
proofend;

theorem :: MEMBER_1:91
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A ** C c= B ** D
proofend;

theorem Th92: :: MEMBER_1:92
for A, B, C being complex-membered set holds A ** (B \/ C) = (A ** B) \/ (A ** C)
proofend;

theorem Th93: :: MEMBER_1:93
for A, B, C being complex-membered set holds A ** (B /\ C) c= (A ** B) /\ (A ** C)
proofend;

theorem Th94: :: MEMBER_1:94
for A, B being complex-membered set holds A ** (-- B) = -- (A ** B)
proofend;

theorem Th95: :: MEMBER_1:95
for A, B, C being complex-membered set holds A ** (B ++ C) c= (A ** B) ++ (A ** C)
proofend;

theorem Th96: :: MEMBER_1:96
for A, B, C being complex-membered set holds A ** (B -- C) c= (A ** B) -- (A ** C)
proofend;

theorem Th97: :: MEMBER_1:97
for A, B being complex-membered set holds (A ** B) "" = (A "") ** (B "")
proofend;

theorem Th98: :: MEMBER_1:98
for a, b being complex number holds {a} ** {b} = {(a * b)}
proofend;

theorem Th99: :: MEMBER_1:99
for a, s, t being complex number holds {a} ** {s,t} = {(a * s),(a * t)}
proofend;

theorem Th100: :: MEMBER_1:100
for a, b, s, t being complex number holds {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)}
proofend;

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

:: deftheorem  defines /// MEMBER_1:def_11_:_
 for F, G being ext-real-membered set holds F /// G = F ** (G "");

theorem Th101: :: MEMBER_1:101
for F, G being ext-real-membered set holds F /// G =  {  (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G )  }
proofend;

theorem Th102: :: MEMBER_1:102
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f / g in F /// G
proofend;

registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF /// G ->  empty ;
coherence
 F /// G is empty ;
clusterG /// F ->  empty ;
coherence
 G /// F is empty ;
end;

registration
let F, G be non empty ext-real-membered set ;
clusterF /// G ->  non empty ;
coherence
 not F /// G is empty ;
end;

registration
let F, G be ext-real-membered set ;
clusterF /// G ->  ext-real-membered ;
coherence
 F /// G is ext-real-membered ;
end;

theorem :: MEMBER_1:103
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F /// H c= G /// I
proofend;

theorem :: MEMBER_1:104
for F, G, H being ext-real-membered set holds (F \/ G) /// H = (F /// H) \/ (G /// H) by Th82;

theorem :: MEMBER_1:105
for F, G, H being ext-real-membered set holds (F /\ G) /// H c= (F /// H) /\ (G /// H) by Th83;

theorem :: MEMBER_1:106
for F, G, H being ext-real-membered set holds F /// (G \/ H) = (F /// G) \/ (F /// H)
proofend;

theorem :: MEMBER_1:107
for F, G, H being ext-real-membered set holds F /// (G /\ H) c= (F /// G) /\ (F /// H)
proofend;

theorem :: MEMBER_1:108
for F, G, H being ext-real-membered set holds (F ** G) /// H = F ** (G /// H) by Th80;

theorem :: MEMBER_1:109
for F, G, H being ext-real-membered set holds (F /// G) ** H = (F ** H) /// G by Th80;

theorem :: MEMBER_1:110
for F, G, H being ext-real-membered set holds (F /// G) /// H = F /// (G ** H)
proofend;

theorem :: MEMBER_1:111
for f, g being ext-real number holds {f} /// {g} = {(f / g)}
proofend;

theorem :: MEMBER_1:112
for f, h, i being ext-real number holds {f} /// {h,i} = {(f / h),(f / i)}
proofend;

theorem :: MEMBER_1:113
for f, g, h being ext-real number holds {f,g} /// {h} = {(f / h),(g / h)}
proofend;

theorem :: MEMBER_1:114
for f, g, h, i being ext-real number holds {f,g} /// {h,i} = {(f / h),(f / i),(g / h),(g / i)}
proofend;

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

:: deftheorem  defines /// MEMBER_1:def_12_:_
 for A, B being complex-membered set holds A /// B = A ** (B "");

theorem Th115: :: MEMBER_1:115
for A, B being complex-membered set holds A /// B =  {  (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B )  }
proofend;

theorem Th116: :: MEMBER_1:116
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a / b in A /// B
proofend;

registration
let A be empty set ;
let B be complex-membered set ;
clusterA /// B ->  empty ;
coherence
 A /// B is empty ;
clusterB /// A ->  empty ;
coherence
 B /// A is empty ;
end;

registration
let A, B be non empty complex-membered set ;
clusterA /// B ->  non empty ;
coherence
 not A /// B is empty ;
end;

registration
let A, B be complex-membered set ;
clusterA /// B ->  complex-membered ;
coherence
 A /// B is complex-membered ;
end;

registration
let A, B be real-membered set ;
clusterA /// B ->  real-membered ;
coherence
 A /// B is real-membered ;
end;

registration
let A, B be rational-membered set ;
clusterA /// B ->  rational-membered ;
coherence
 A /// B is rational-membered ;
end;

registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA /// B with F /// G when A = F, B = G;
compatibility
 ( A = F & B = G implies A /// B = F /// G ) ;
end;

theorem :: MEMBER_1:117
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A /// C c= B /// D
proofend;

theorem :: MEMBER_1:118
for A, B, C being complex-membered set holds A /// (B \/ C) = (A /// B) \/ (A /// C)
proofend;

theorem :: MEMBER_1:119
for A, B, C being complex-membered set holds A /// (B /\ C) c= (A /// B) /\ (A /// C)
proofend;

theorem :: MEMBER_1:120
for A, B being complex-membered set holds A /// (-- B) = -- (A /// B)
proofend;

theorem :: MEMBER_1:121
for A, B being complex-membered set holds (-- A) /// B = -- (A /// B) by Th94;

theorem :: MEMBER_1:122
for A, B, C being complex-membered set holds (A ++ B) /// C c= (A /// C) ++ (B /// C) by Th95;

theorem :: MEMBER_1:123
for A, B, C being complex-membered set holds (A -- B) /// C c= (A /// C) -- (B /// C)
proofend;

theorem :: MEMBER_1:124
for A, B, C being complex-membered set holds (A ** B) /// C = A ** (B /// C) by Th90;

theorem :: MEMBER_1:125
for A, B, C being complex-membered set holds (A /// B) ** C = (A ** C) /// B by Th90;

theorem :: MEMBER_1:126
for A, B, C being complex-membered set holds (A /// B) /// C = A /// (B ** C)
proofend;

theorem :: MEMBER_1:127
for A, B, C being complex-membered set holds A /// (B /// C) = (A ** C) /// B
proofend;

theorem :: MEMBER_1:128
for a, b being complex number holds {a} /// {b} = {(a / b)}
proofend;

theorem :: MEMBER_1:129
for a, s, t being complex number holds {a} /// {s,t} = {(a / s),(a / t)}
proofend;

theorem :: MEMBER_1:130
for a, b, s being complex number holds {a,b} /// {s} = {(a / s),(b / s)}
proofend;

theorem :: MEMBER_1:131
for a, b, s, t being complex number holds {a,b} /// {s,t} = {(a / s),(a / t),(b / s),(b / t)}
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf ++ F ->  set  equals :: MEMBER_1:def 13
{f} ++ F;
coherence
 {f} ++ F is set ;
end;

:: deftheorem  defines ++ MEMBER_1:def_13_:_
 for F being ext-real-membered set
for f being ext-real number holds f ++ F = {f} ++ F;

theorem Th132: :: MEMBER_1:132
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f + g in f ++ G
proofend;

theorem Th133: :: MEMBER_1:133
for F being ext-real-membered set
for f being ext-real number holds f ++ F =  {  (f + w) where w is Element of ExtREAL : w in F  }
proofend;

theorem Th134: :: MEMBER_1:134
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterf ++ F ->  empty ;
coherence
 f ++ F is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf ++ F ->  non empty ;
coherence
 not f ++ F is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf ++ F ->  ext-real-membered ;
coherence
 f ++ F is ext-real-membered ;
end;

theorem Th135: :: MEMBER_1:135
for F, G being ext-real-membered set
for r being real number st r ++ F c= r ++ G holds
F c= G
proofend;

theorem :: MEMBER_1:136
for F, G being ext-real-membered set
for r being real number st r ++ F = r ++ G holds
F = G
proofend;

theorem Th137: :: MEMBER_1:137
for F, G being ext-real-membered set
for r being real number holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
proofend;

theorem Th138: :: MEMBER_1:138
for F, G being ext-real-membered set
for f being ext-real number holds (f ++ F) \ (f ++ G) c= f ++ (F \ G)
proofend;

theorem Th139: :: MEMBER_1:139
for F, G being ext-real-membered set
for r being real number holds r ++ (F \ G) = (r ++ F) \ (r ++ G)
proofend;

theorem Th140: :: MEMBER_1:140
for F, G being ext-real-membered set
for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)
proofend;

definition
let A be complex-membered set ;
let a be complex number ;
funca ++ A ->  set  equals :: MEMBER_1:def 14
{a} ++ A;
coherence
 {a} ++ A is set ;
end;

:: deftheorem  defines ++ MEMBER_1:def_14_:_
 for A being complex-membered set
for a being complex number holds a ++ A = {a} ++ A;

theorem Th141: :: MEMBER_1:141
for A being complex-membered set
for b, a being complex number st b in A holds
a + b in a ++ A
proofend;

theorem Th142: :: MEMBER_1:142
for A being complex-membered set
for a being complex number holds a ++ A =  {  (a + c) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th143: :: MEMBER_1:143
for A being complex-membered set
for a being complex number
for e being set st e in a ++ A holds
ex c being Element of COMPLEX st
( e = a + c & c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clustera ++ A ->  empty ;
coherence
 a ++ A is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera ++ A ->  non empty ;
coherence
 not a ++ A is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clustera ++ A ->  complex-membered ;
coherence
 a ++ A is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clustera ++ A ->  real-membered ;
coherence
 a ++ A is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clustera ++ A ->  rational-membered ;
coherence
 a ++ A is rational-membered ;
end;

registration
let A be integer-membered set ;
let a be integer number ;
clustera ++ A ->  integer-membered ;
coherence
 a ++ A is integer-membered ;
end;

registration
let A be natural-membered set ;
let a be Nat;
clustera ++ A ->  natural-membered ;
coherence
 a ++ A is natural-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya ++ A with f ++ F when A = F, a = f;
compatibility
 ( A = F & a = f implies a ++ A = f ++ F ) ;
end;

theorem Th144: :: MEMBER_1:144
for A, B being complex-membered set
for a being complex number holds
( A c= B iff a ++ A c= a ++ B )
proofend;

theorem :: MEMBER_1:145
for A, B being complex-membered set
for a being complex number st a ++ A = a ++ B holds
A = B
proofend;

theorem :: MEMBER_1:146
for A being complex-membered set holds 0 ++ A = A
proofend;

theorem :: MEMBER_1:147
for A being complex-membered set
for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A)
proofend;

theorem :: MEMBER_1:148
for A, B being complex-membered set
for a being complex number holds a ++ (A ++ B) = (a ++ A) ++ B by Th50;

theorem Th149: :: MEMBER_1:149
for A, B being complex-membered set
for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
proofend;

theorem Th150: :: MEMBER_1:150
for A, B being complex-membered set
for a being complex number holds a ++ (A \ B) = (a ++ A) \ (a ++ B)
proofend;

theorem Th151: :: MEMBER_1:151
for A, B being complex-membered set
for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf -- F ->  set  equals :: MEMBER_1:def 15
{f} -- F;
coherence
 {f} -- F is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_15_:_
 for F being ext-real-membered set
for f being ext-real number holds f -- F = {f} -- F;

theorem Th152: :: MEMBER_1:152
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f - g in f -- G
proofend;

theorem Th153: :: MEMBER_1:153
for F being ext-real-membered set
for f being ext-real number holds f -- F =  {  (f - w) where w is Element of ExtREAL : w in F  }
proofend;

theorem Th154: :: MEMBER_1:154
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f -- F holds
ex w being Element of ExtREAL st
( e = f - w & w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterf -- F ->  empty ;
coherence
 f -- F is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf -- F ->  non empty ;
coherence
 not f -- F is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf -- F ->  ext-real-membered ;
coherence
 f -- F is ext-real-membered ;
end;

theorem Th155: :: MEMBER_1:155
for F, G being ext-real-membered set
for r being real number st r -- F c= r -- G holds
F c= G
proofend;

theorem :: MEMBER_1:156
for F, G being ext-real-membered set
for r being real number st r -- F = r -- G holds
F = G
proofend;

theorem Th157: :: MEMBER_1:157
for F, G being ext-real-membered set
for r being real number holds r -- (F /\ G) = (r -- F) /\ (r -- G)
proofend;

theorem Th158: :: MEMBER_1:158
for F, G being ext-real-membered set
for r being real number holds r -- (F \ G) = (r -- F) \ (r -- G)
proofend;

theorem Th159: :: MEMBER_1:159
for F, G being ext-real-membered set
for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)
proofend;

definition
let A be complex-membered set ;
let a be complex number ;
funca -- A ->  set  equals :: MEMBER_1:def 16
{a} -- A;
coherence
 {a} -- A is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_16_:_
 for A being complex-membered set
for a being complex number holds a -- A = {a} -- A;

theorem Th160: :: MEMBER_1:160
for A being complex-membered set
for b, a being complex number st b in A holds
a - b in a -- A
proofend;

theorem Th161: :: MEMBER_1:161
for A being complex-membered set
for a being complex number holds a -- A =  {  (a - c) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th162: :: MEMBER_1:162
for A being complex-membered set
for a being complex number
for e being set st e in a -- A holds
ex c being Element of COMPLEX st
( e = a - c & c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clustera -- A ->  empty ;
coherence
 a -- A is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera -- A ->  non empty ;
coherence
 not a -- A is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clustera -- A ->  complex-membered ;
coherence
 a -- A is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clustera -- A ->  real-membered ;
coherence
 a -- A is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clustera -- A ->  rational-membered ;
coherence
 a -- A is rational-membered ;
end;

registration
let A be integer-membered set ;
let a be integer number ;
clustera -- A ->  integer-membered ;
coherence
 a -- A is integer-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya -- A with f -- F when A = F, a = f;
compatibility
 ( A = F & a = f implies a -- A = f -- F ) ;
end;

theorem Th163: :: MEMBER_1:163
for A, B being complex-membered set
for a being complex number holds
( A c= B iff a -- A c= a -- B )
proofend;

theorem :: MEMBER_1:164
for A, B being complex-membered set
for a being complex number st a -- A = a -- B holds
A = B
proofend;

theorem Th165: :: MEMBER_1:165
for A, B being complex-membered set
for a being complex number holds a -- (A /\ B) = (a -- A) /\ (a -- B)
proofend;

theorem Th166: :: MEMBER_1:166
for A, B being complex-membered set
for a being complex number holds a -- (A \ B) = (a -- A) \ (a -- B)
proofend;

theorem Th167: :: MEMBER_1:167
for A, B being complex-membered set
for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcF -- f ->  set  equals :: MEMBER_1:def 17
F -- {f};
coherence
 F -- {f} is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_17_:_
 for F being ext-real-membered set
for f being ext-real number holds F -- f = F -- {f};

theorem Th168: :: MEMBER_1:168
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
g - f in G -- f
proofend;

theorem Th169: :: MEMBER_1:169
for F being ext-real-membered set
for f being ext-real number holds F -- f =  {  (w - f) where w is Element of ExtREAL : w in F  }
proofend;

theorem :: MEMBER_1:170
for F being ext-real-membered set
for f being ext-real number
for e being set st e in F -- f holds
ex w being Element of ExtREAL st
( e = w - f & w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterF -- f ->  empty ;
coherence
 F -- f is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterF -- f ->  non empty ;
coherence
 not F -- f is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterF -- f ->  ext-real-membered ;
coherence
 F -- f is ext-real-membered ;
end;

theorem :: MEMBER_1:171
for F being ext-real-membered set
for f being ext-real number holds F -- f = -- (f -- F) by Th60;

theorem :: MEMBER_1:172
for F being ext-real-membered set
for f being ext-real number holds f -- F = -- (F -- f) by Th60;

theorem :: MEMBER_1:173
for F, G being ext-real-membered set
for r being real number holds (F /\ G) -- r = (F -- r) /\ (G -- r)
proofend;

theorem :: MEMBER_1:174
for F, G being ext-real-membered set
for r being real number holds (F \ G) -- r = (F -- r) \ (G -- r)
proofend;

theorem :: MEMBER_1:175
for F, G being ext-real-membered set
for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)
proofend;

definition
let A be complex-membered set ;
let a be complex number ;
funcA -- a ->  set  equals :: MEMBER_1:def 18
A -- {a};
coherence
 A -- {a} is set ;
end;

:: deftheorem  defines -- MEMBER_1:def_18_:_
 for A being complex-membered set
for a being complex number holds A -- a = A -- {a};

theorem Th176: :: MEMBER_1:176
for A being complex-membered set
for b, a being complex number st b in A holds
b - a in A -- a
proofend;

theorem Th177: :: MEMBER_1:177
for A being complex-membered set
for a being complex number holds A -- a =  {  (c - a) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th178: :: MEMBER_1:178
for A being complex-membered set
for a being complex number
for e being set st e in A -- a holds
ex c being Element of COMPLEX st
( e = c - a & c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clusterA -- a ->  empty ;
coherence
 A -- a is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clusterA -- a ->  non empty ;
coherence
 not A -- a is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clusterA -- a ->  complex-membered ;
coherence
 A -- a is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clusterA -- a ->  real-membered ;
coherence
 A -- a is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clusterA -- a ->  rational-membered ;
coherence
 A -- a is rational-membered ;
end;

registration
let A be integer-membered set ;
let a be integer number ;
clusterA -- a ->  integer-membered ;
coherence
 A -- a is integer-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifyA -- a with F -- f when A = F, a = f;
compatibility
 ( A = F & a = f implies A -- a = F -- f ) ;
end;

theorem Th179: :: MEMBER_1:179
for A, B being complex-membered set
for a being complex number holds
( A c= B iff A -- a c= B -- a )
proofend;

theorem :: MEMBER_1:180
for A, B being complex-membered set
for a being complex number st A -- a = B -- a holds
A = B
proofend;

theorem :: MEMBER_1:181
for A being complex-membered set
for a being complex number holds A -- a = -- (a -- A) by Th71;

theorem :: MEMBER_1:182
for A being complex-membered set
for a being complex number holds a -- A = -- (A -- a) by Th71;

theorem :: MEMBER_1:183
for A, B being complex-membered set
for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a)
proofend;

theorem :: MEMBER_1:184
for A, B being complex-membered set
for a being complex number holds (A \ B) -- a = (A -- a) \ (B -- a)
proofend;

theorem :: MEMBER_1:185
for A, B being complex-membered set
for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a)
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf ** F ->  set  equals :: MEMBER_1:def 19
{f} ** F;
coherence
 {f} ** F is set ;
end;

:: deftheorem  defines ** MEMBER_1:def_19_:_
 for F being ext-real-membered set
for f being ext-real number holds f ** F = {f} ** F;

theorem Th186: :: MEMBER_1:186
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f * g in f ** G
proofend;

theorem Th187: :: MEMBER_1:187
for F being ext-real-membered set
for f being ext-real number holds f ** F =  {  (f * w) where w is Element of ExtREAL : w in F  }
proofend;

theorem Th188: :: MEMBER_1:188
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f ** F holds
ex w being Element of ExtREAL st
( e = f * w & w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterf ** F ->  empty ;
coherence
 f ** F is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf ** F ->  non empty ;
coherence
 not f ** F is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf ** F ->  ext-real-membered ;
coherence
 f ** F is ext-real-membered ;
end;

theorem :: MEMBER_1:189
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F /\ G) = (r ** F) /\ (r ** G)
proofend;

theorem Th190: :: MEMBER_1:190
for F, G being ext-real-membered set
for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G)
proofend;

theorem Th191: :: MEMBER_1:191
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F \ G) = (r ** F) \ (r ** G)
proofend;

theorem :: MEMBER_1:192
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)
proofend;

definition
let A be complex-membered set ;
let a be complex number ;
funca ** A ->  set  equals :: MEMBER_1:def 20
{a} ** A;
coherence
 {a} ** A is set ;
end;

:: deftheorem  defines ** MEMBER_1:def_20_:_
 for A being complex-membered set
for a being complex number holds a ** A = {a} ** A;

theorem Th193: :: MEMBER_1:193
for A being complex-membered set
for b, a being complex number st b in A holds
a * b in a ** A
proofend;

theorem Th194: :: MEMBER_1:194
for A being complex-membered set
for a being complex number holds a ** A =  {  (a * c) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th195: :: MEMBER_1:195
for A being complex-membered set
for a being complex number
for e being set st e in a ** A holds
ex c being Element of COMPLEX st
( e = a * c &amp; c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clustera ** A ->  empty ;
coherence
 a ** A is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera ** A ->  non empty ;
coherence
 not a ** A is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clustera ** A ->  complex-membered ;
coherence
 a ** A is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clustera ** A ->  real-membered ;
coherence
 a ** A is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clustera ** A ->  rational-membered ;
coherence
 a ** A is rational-membered ;
end;

registration
let A be integer-membered set ;
let a be integer number ;
clustera ** A ->  integer-membered ;
coherence
 a ** A is integer-membered ;
end;

registration
let A be natural-membered set ;
let a be Nat;
clustera ** A ->  natural-membered ;
coherence
 a ** A is natural-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya ** A with f ** F when A = F, a = f;
compatibility
 ( A = F &amp; a = f implies a ** A = f ** F ) ;
end;

theorem Th196: :: MEMBER_1:196
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; a ** A c= a ** B holds
A c= B
proofend;

theorem :: MEMBER_1:197
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; a ** A = a ** B holds
A = B
proofend;

theorem Th198: :: MEMBER_1:198
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A /\ B) = (a ** A) /\ (a ** B)
proofend;

theorem Th199: :: MEMBER_1:199
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A \ B) = (a ** A) \ (a ** B)
proofend;

theorem Th200: :: MEMBER_1:200
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A \+\ B) = (a ** A) \+\ (a ** B)
proofend;

theorem Th201: :: MEMBER_1:201
for A being complex-membered set holds 0 ** A c= {0}
proofend;

theorem :: MEMBER_1:202
for A being complex-membered set st A <> {} holds
0 ** A = {0}
proofend;

theorem :: MEMBER_1:203
for A being complex-membered set holds 1 ** A = A
proofend;

theorem :: MEMBER_1:204
for A being complex-membered set
for a, b being complex number holds (a * b) ** A = a ** (b ** A)
proofend;

theorem :: MEMBER_1:205
for A, B being complex-membered set
for a being complex number holds a ** (A ** B) = (a ** A) ** B by Th90;

theorem :: MEMBER_1:206
for A being complex-membered set
for a, b being complex number holds (a + b) ** A c= (a ** A) ++ (b ** A)
proofend;

theorem :: MEMBER_1:207
for A being complex-membered set
for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A)
proofend;

theorem Th208: :: MEMBER_1:208
for B, C being complex-membered set
for a being complex number holds a ** (B ++ C) = (a ** B) ++ (a ** C)
proofend;

theorem :: MEMBER_1:209
for B, C being complex-membered set
for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C)
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf /// F ->  set  equals :: MEMBER_1:def 21
{f} /// F;
coherence
 {f} /// F is set ;
end;

:: deftheorem  defines /// MEMBER_1:def_21_:_
 for F being ext-real-membered set
for f being ext-real number holds f /// F = {f} /// F;

theorem Th210: :: MEMBER_1:210
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f / g in f /// G
proofend;

theorem Th211: :: MEMBER_1:211
for F being ext-real-membered set
for f being ext-real number holds f /// F =  {  (f / w) where w is Element of ExtREAL : w in F  }
proofend;

theorem :: MEMBER_1:212
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f /// F holds
ex w being Element of ExtREAL st
( e = f / w &amp; w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterf /// F ->  empty ;
coherence
 f /// F is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf /// F ->  non empty ;
coherence
 not f /// F is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf /// F ->  ext-real-membered ;
coherence
 f /// F is ext-real-membered ;
end;

definition
let A be complex-membered set ;
let a be complex number ;
funca /// A ->  set  equals :: MEMBER_1:def 22
{a} /// A;
coherence
 {a} /// A is set ;
end;

:: deftheorem  defines /// MEMBER_1:def_22_:_
 for A being complex-membered set
for a being complex number holds a /// A = {a} /// A;

theorem Th213: :: MEMBER_1:213
for A being complex-membered set
for b, a being complex number st b in A holds
a / b in a /// A
proofend;

theorem Th214: :: MEMBER_1:214
for A being complex-membered set
for a being complex number holds a /// A =  {  (a / c) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th215: :: MEMBER_1:215
for A being complex-membered set
for a being complex number
for e being set st e in a /// A holds
ex c being Element of COMPLEX st
( e = a / c &amp; c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clustera /// A ->  empty ;
coherence
 a /// A is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera /// A ->  non empty ;
coherence
 not a /// A is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clustera /// A ->  complex-membered ;
coherence
 a /// A is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clustera /// A ->  real-membered ;
coherence
 a /// A is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clustera /// A ->  rational-membered ;
coherence
 a /// A is rational-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya /// A with f /// F when A = F, a = f;
compatibility
 ( A = F &amp; a = f implies a /// A = f /// F ) ;
end;

theorem Th216: :: MEMBER_1:216
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; a /// A c= a /// B holds
A c= B
proofend;

theorem :: MEMBER_1:217
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; a /// A = a /// B holds
A = B
proofend;

theorem :: MEMBER_1:218
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A /\ B) = (a /// A) /\ (a /// B)
proofend;

theorem :: MEMBER_1:219
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A \ B) = (a /// A) \ (a /// B)
proofend;

theorem :: MEMBER_1:220
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A \+\ B) = (a /// A) \+\ (a /// B)
proofend;

theorem :: MEMBER_1:221
for A being complex-membered set
for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A)
proofend;

theorem :: MEMBER_1:222
for A being complex-membered set
for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A)
proofend;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcF /// f ->  set  equals :: MEMBER_1:def 23
F /// {f};
coherence
 F /// {f} is set ;
end;

:: deftheorem  defines /// MEMBER_1:def_23_:_
 for F being ext-real-membered set
for f being ext-real number holds F /// f = F /// {f};

theorem Th223: :: MEMBER_1:223
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
g / f in G /// f
proofend;

theorem Th224: :: MEMBER_1:224
for F being ext-real-membered set
for f being ext-real number holds F /// f =  {  (w / f) where w is Element of ExtREAL : w in F  }
proofend;

theorem :: MEMBER_1:225
for F being ext-real-membered set
for f being ext-real number
for e being set st e in F /// f holds
ex w being Element of ExtREAL st
( e = w / f &amp; w in F )
proofend;

registration
let F be empty set ;
let f be ext-real number ;
clusterF /// f ->  empty ;
coherence
 F /// f is empty ;
end;

registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterF /// f ->  non empty ;
coherence
 not F /// f is empty ;
end;

registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterF /// f ->  ext-real-membered ;
coherence
 F /// f is ext-real-membered ;
end;

definition
let A be complex-membered set ;
let a be complex number ;
funcA /// a ->  set  equals :: MEMBER_1:def 24
A /// {a};
coherence
 A /// {a} is set ;
end;

:: deftheorem  defines /// MEMBER_1:def_24_:_
 for A being complex-membered set
for a being complex number holds A /// a = A /// {a};

theorem Th226: :: MEMBER_1:226
for A being complex-membered set
for b, a being complex number st b in A holds
b / a in A /// a
proofend;

theorem Th227: :: MEMBER_1:227
for A being complex-membered set
for a being complex number holds A /// a =  {  (c / a) where c is Element of COMPLEX : c in A  }
proofend;

theorem Th228: :: MEMBER_1:228
for A being complex-membered set
for a being complex number
for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a &amp; c in A )
proofend;

registration
let A be empty set ;
let a be complex number ;
clusterA /// a ->  empty ;
coherence
 A /// a is empty ;
end;

registration
let A be non empty complex-membered set ;
let a be complex number ;
clusterA /// a ->  non empty ;
coherence
 not A /// a is empty ;
end;

registration
let A be complex-membered set ;
let a be complex number ;
clusterA /// a ->  complex-membered ;
coherence
 A /// a is complex-membered ;
end;

registration
let A be real-membered set ;
let a be real number ;
clusterA /// a ->  real-membered ;
coherence
 A /// a is real-membered ;
end;

registration
let A be rational-membered set ;
let a be rational number ;
clusterA /// a ->  rational-membered ;
coherence
 A /// a is rational-membered ;
end;

registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifyA /// a with F /// f when A = F, a = f;
compatibility
 ( A = F &amp; a = f implies A /// a = F /// f ) ;
end;

theorem Th229: :: MEMBER_1:229
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; A /// a c= B /// a holds
A c= B
proofend;

theorem :: MEMBER_1:230
for A, B being complex-membered set
for a being complex number st a <> 0 &amp; A /// a = B /// a holds
A = B
proofend;

theorem :: MEMBER_1:231
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A /\ B) /// a = (A /// a) /\ (B /// a)
proofend;

theorem :: MEMBER_1:232
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A \ B) /// a = (A /// a) \ (B /// a)
proofend;

theorem :: MEMBER_1:233
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A \+\ B) /// a = (A /// a) \+\ (B /// a)
proofend;

theorem Th234: :: MEMBER_1:234
for A, B being complex-membered set
for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a)
proofend;

theorem :: MEMBER_1:235
for A, B being complex-membered set
for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a)
proofend;