:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008 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 func w " -> Element of ExtREAL ;
coherence
w " is Element of ExtREAL by XXREAL_0:def 1;
let w1 be Element of ExtREAL ;
:: original: *
redefine func w * 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
proof end;
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
proof end;
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
proof end;
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 }
proof end;
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 )
proof end;

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 )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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
proof end;
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 }
proof end;
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 )
proof end;

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

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

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

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

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

registration
let A be integer-membered set ;
cluster -- A -> complex-membered integer-membered ;
coherence
-- A is integer-membered
proof end;
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 )
proof end;
end;

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

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

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

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

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

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

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

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

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

definition
let F be ext-real-membered set ;
func F "" -> 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
proof end;
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 ""
proof end;

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

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

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

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

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

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

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

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

definition
let A be complex-membered set ;
func A "" -> 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
proof end;
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 }
proof end;
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 "" )
proof end;

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

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

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

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

registration
let A be rational-membered set ;
cluster A "" -> complex-membered rational-membered ;
coherence
A "" is rational-membered
proof end;
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 "" )
proof end;
end;

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

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

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

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

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

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

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

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

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

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

definition
let F, G be ext-real-membered set ;
func F ++ 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 ) }
proof end;
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
proof end;

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

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

registration
let F, G be ext-real-membered set ;
cluster F ++ G -> ext-real-membered ;
coherence
F ++ G is ext-real-membered
proof end;
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
proof end;

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

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

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

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

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)}
proof end;

definition
let A, B be complex-membered set ;
func A ++ 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 ) }
proof end;
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
proof end;

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

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

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

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

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

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

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

registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identify A ++ B with F ++ G when A = F, B = G;
compatibility
( A = F & B = G implies A ++ B = F ++ G )
proof end;
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
proof end;

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

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

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

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

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

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)}
proof end;

definition
let F, G be ext-real-membered set ;
func F -- 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 ) }
proof end;

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
proof end;

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

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

registration
let F, G be ext-real-membered set ;
cluster F -- 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
proof end;

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

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

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

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
proof end;

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

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

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

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)}
proof end;

definition
let A, B be complex-membered set ;
func A -- 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 ) }
proof end;

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
proof end;

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

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

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

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

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

registration
let A, B be integer-membered set ;
cluster A -- 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 ;
identify A -- 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
proof end;

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

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

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

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
proof end;

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
proof end;

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

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

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

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

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)}
proof end;

definition
let F, G be ext-real-membered set ;
func F ** 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 ) }
proof end;
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 ;
cluster F ** G -> empty ;
coherence
F ** G is empty
proof end;
cluster G ** F -> empty ;
coherence
G ** F is empty ;
end;

registration
let F, G be ext-real-membered set ;
cluster F ** G -> ext-real-membered ;
coherence
F ** G is ext-real-membered
proof end;
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
proof end;

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

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

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
proof end;

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

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

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

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

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

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

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)}
proof end;

definition
let A, B be complex-membered set ;
func A ** 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 ) }
proof end;
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
proof end;

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

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

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

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

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

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

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

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

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

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
proof end;

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

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

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

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

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

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

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

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

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)}
proof end;

definition
let F, G be ext-real-membered set ;
func F /// 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 ) }
proof end;

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
proof end;

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

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

registration
let F, G be ext-real-membered set ;
cluster F /// 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
proof end;

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)
proof end;

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

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)
proof end;

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

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

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

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)}
proof end;

definition
let A, B be complex-membered set ;
func A /// 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 ) }
proof end;

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
proof end;

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

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

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

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

registration
let A, B be rational-membered set ;
cluster A /// 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 ;
identify A /// 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
proof end;

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

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

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

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)
proof end;

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)
proof end;

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

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

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

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

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)}
proof end;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func f ++ 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

registration
let F be ext-real-membered set ;
let f be ext-real number ;
cluster f ++ 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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

definition
let A be complex-membered set ;
let a be complex number ;
func a ++ 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

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

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

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

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

registration
let A be natural-membered set ;
let a be natural number ;
cluster a ++ 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 ;
identify a ++ 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 )
proof end;

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

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

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

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)
proof end;

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)
proof end;

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)
proof end;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func f -- 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

registration
let F be ext-real-membered set ;
let f be ext-real number ;
cluster f -- 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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

definition
let A be complex-membered set ;
let a be complex number ;
func a -- 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

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

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

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

registration
let A be integer-membered set ;
let a be integer number ;
cluster a -- 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 ;
identify a -- 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 )
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func F -- 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

registration
let F be ext-real-membered set ;
let f be ext-real number ;
cluster F -- 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)
proof end;

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)
proof end;

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)
proof end;

definition
let A be complex-membered set ;
let a be complex number ;
func A -- 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

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

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

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

registration
let A be integer-membered set ;
let a be integer number ;
cluster A -- 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 ;
identify A -- 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 )
proof end;

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

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)
proof end;

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

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

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func f ** 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
proof end;

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 }
proof end;

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 )
proof end;

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

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

registration
let F be ext-real-membered set ;
let f be ext-real number ;
cluster f ** 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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

definition
let A be complex-membered set ;
let a be complex number ;
func a ** 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
proof end;

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 }
proof end;

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 & c in A )
proof end;

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

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

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

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

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

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

registration
let A be natural-membered set ;
let a be natural number ;
cluster a ** 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 ;
identify a ** A with f ** F when A = F, a = f;
compatibility
( A = F & 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 & a ** A c= a ** B holds
A c= B
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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

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

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

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

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)
proof end;

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)
proof end;

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)
proof end;

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

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func f /// 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
proof end;

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 }
proof end;

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 & w in F )
proof end;

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

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

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

definition
let A be complex-membered set ;
let a be complex number ;
func a /// 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
proof end;

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 }
proof end;

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 & c in A )
proof end;

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

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

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

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

registration
let A be rational-membered set ;
let a be rational number ;
cluster a /// 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 ;
identify a /// A with f /// F when A = F, a = f;
compatibility
( A = F & 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 & a /// A c= a /// B holds
A c= B
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

definition
let F be ext-real-membered set ;
let f be ext-real number ;
func F /// 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
proof end;

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 }
proof end;

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 & w in F )
proof end;

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

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

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

definition
let A be complex-membered set ;
let a be complex number ;
func A /// 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
proof end;

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 }
proof end;

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 & c in A )
proof end;

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

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

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

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

registration
let A be rational-membered set ;
let a be rational number ;
cluster A /// 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 ;
identify A /// a with F /// f when A = F, a = f;
compatibility
( A = F & 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 & A /// a c= B /// a holds
A c= B
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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