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

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;

cluster {a,b,c,d} -> complex-membered ;

coherence
{a,b,c,d} is complex-membered by ENUMSET1:def 2;

end;

registration

let a, b, c, d be ExtReal;

cluster {a,b,c,d} -> ext-real-membered ;

coherence
{a,b,c,d} is ext-real-membered by ENUMSET1:def 2;

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 b₁, b₂ being ext-real-membered set st b₁ = { (- w) where w is Element of ExtREAL : w in b₂ } holds
b₂ = { (- w) where w is Element of ExtREAL : w in b₁ }

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 ExtReal 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 ExtReal holds
( - f in F iff f in -- F )

proof end;

registration

let F be empty set ;

cluster -- F -> ext-real-membered empty ;

coherence
-- F is empty

proof end;

end;

registration

let F be ext-real-membered non empty set ;

cluster -- F -> ext-real-membered non empty ;

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 ExtReal holds -- {f} = {(- f)}

proof end;

theorem Th10: :: MEMBER_1:10

for f, g being ExtReal 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 Complex : c in A } ;

coherence
{ (- c) where c is Complex : c in A } is complex-membered set

proof end;

involutiveness
for b₁, b₂ being complex-membered set st b₁ = { (- c) where c is Complex : c in b₂ } holds
b₂ = { (- c) where c is Complex : c in b₁ }

proof end;

end;

:: deftheorem defines -- MEMBER_1:def 2 :
for A being complex-membered set holds -- A = { (- c) where c is Complex : c in A } ;

theorem Th11: :: MEMBER_1:11

for A being complex-membered set
for a being Complex 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 holds
( - a in A iff a in -- A )

proof end;

registration

let A be empty set ;

cluster -- A -> complex-membered empty ;

coherence
-- A is empty

proof end;

end;

registration

let A be complex-membered non empty set ;

cluster -- A -> complex-membered non empty ;

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 holds -- {a} = {(- a)}

proof end;

theorem Th20: :: MEMBER_1:20

for a, b being Complex 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 ExtReal st f in F holds
f " in F ""

proof end;

registration

let F be empty set ;

cluster F "" -> ext-real-membered empty ;

coherence
F "" is empty

proof end;

end;

registration

let F be ext-real-membered non empty set ;

cluster F "" -> ext-real-membered non empty ;

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 ExtReal holds {f} "" = {(f ")}

proof end;

theorem Th27: :: MEMBER_1:27

for f, g being ExtReal 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 Complex : c in A } ;

coherence
{ (c ") where c is Complex : c in A } is complex-membered set

proof end;

involutiveness
for b₁, b₂ being complex-membered set st b₁ = { (c ") where c is Complex : c in b₂ } holds
b₂ = { (c ") where c is Complex : c in b₁ }

proof end;

end;

:: deftheorem defines "" MEMBER_1:def 4 :
for A being complex-membered set holds A "" = { (c ") where c is Complex : c in A } ;

theorem Th28: :: MEMBER_1:28

for A being complex-membered set
for a being Complex 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 holds
( a " in A iff a in A "" )

proof end;

registration

let A be empty set ;

cluster A "" -> complex-membered empty ;

coherence
A "" is empty

proof end;

end;

registration

let A be complex-membered non empty set ;

cluster A "" -> complex-membered non empty ;

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 holds {a} "" = {(a ")}

proof end;

theorem Th38: :: MEMBER_1:38

for a, b being Complex 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 b₁ being set
for F, G being ext-real-membered set st b₁ = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
b₁ = { (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 ExtReal 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 ext-real-membered non empty 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 ExtReal holds {f} ++ {g} = {(f + g)}

proof end;

theorem Th44: :: MEMBER_1:44

for f, g, h being ExtReal holds {f} ++ {g,h} = {(f + g),(f + h)}

proof end;

theorem Th45: :: MEMBER_1:45

for f, g, h, i being ExtReal 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 Complex : ( c1 in A & c2 in B ) } ;

coherence
{ (c1 + c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } is set ;
commutativity
for b₁ being set
for A, B being complex-membered set st b₁ = { (c1 + c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } holds
b₁ = { (c1 + c2) where c1, c2 is 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 Complex : ( c1 in A & c2 in B ) } ;

theorem :: MEMBER_1:46

for A, B being complex-membered set
for a, b being Complex st a in A & b in B holds
a + b in A ++ B ;

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 complex-membered non empty 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 holds {a} ++ {b} = {(a + b)}

proof end;

theorem Th52: :: MEMBER_1:52

for a, s, t being Complex holds {a} ++ {s,t} = {(a + s),(a + t)}

proof end;

theorem Th53: :: MEMBER_1:53

for a, b, s, t being Complex 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 ExtReal 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 ext-real-membered non empty 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 ExtReal holds {f} -- {g} = {(f - g)}

proof end;

theorem :: MEMBER_1:62

for f, h, i being ExtReal holds {f} -- {h,i} = {(f - h),(f - i)}

proof end;

theorem :: MEMBER_1:63

for f, g, h being ExtReal holds {f,g} -- {h} = {(f - h),(g - h)}

proof end;

theorem :: MEMBER_1:64

for f, g, h, i being ExtReal 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 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 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 complex-membered non empty 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 holds {a} -- {b} = {(a - b)}

proof end;

theorem :: MEMBER_1:76

for a, s, t being Complex holds {a} -- {s,t} = {(a - s),(a - t)}

proof end;

theorem :: MEMBER_1:77

for a, b, s being Complex holds {a,b} -- {s} = {(a - s),(b - s)}

proof end;

theorem :: MEMBER_1:78

for a, b, s, t being Complex 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 b₁ being set
for F, G being ext-real-membered set st b₁ = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
b₁ = { (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 ExtReal st f in F & g in G holds
f * g in F ** G

proof end;

registration

let F, G be ext-real-membered non empty 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 ExtReal holds {f} ** {g} = {(f * g)}

proof end;

theorem Th87: :: MEMBER_1:87

for f, h, i being ExtReal holds {f} ** {h,i} = {(f * h),(f * i)}

proof end;

theorem Th88: :: MEMBER_1:88

for f, g, h, i being ExtReal 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 Complex : ( c1 in A & c2 in B ) } ;

coherence
{ (c1 * c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } is set ;
commutativity
for b₁ being set
for A, B being complex-membered set st b₁ = { (c1 * c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } holds
b₁ = { (c1 * c2) where c1, c2 is 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 Complex : ( c1 in A & c2 in B ) } ;

theorem :: MEMBER_1:89

for A, B being complex-membered set
for a, b being Complex st a in A & b in B holds
a * b in A ** B ;

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 complex-membered non empty 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 holds {a} ** {b} = {(a * b)}

proof end;

theorem Th99: :: MEMBER_1:99

for a, s, t being Complex holds {a} ** {s,t} = {(a * s),(a * t)}

proof end;

theorem Th100: :: MEMBER_1:100

for a, b, s, t being Complex 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 ExtReal 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 ext-real-membered non empty 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 ExtReal holds {f} /// {g} = {(f / g)}

proof end;

theorem :: MEMBER_1:112

for f, h, i being ExtReal holds {f} /// {h,i} = {(f / h),(f / i)}

proof end;

theorem :: MEMBER_1:113

for f, g, h being ExtReal holds {f,g} /// {h} = {(f / h),(g / h)}

proof end;

theorem :: MEMBER_1:114

for f, g, h, i being ExtReal 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 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 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 complex-membered non empty 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 holds {a} /// {b} = {(a / b)}

proof end;

theorem :: MEMBER_1:129

for a, s, t being Complex holds {a} /// {s,t} = {(a / s),(a / t)}

proof end;

theorem :: MEMBER_1:130

for a, b, s being Complex holds {a,b} /// {s} = {(a / s),(b / s)}

proof end;

theorem :: MEMBER_1:131

for a, b, s, t being Complex 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 ExtReal;

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 ExtReal holds f ++ F = {f} ++ F;

theorem Th132: :: MEMBER_1:132

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster f ++ F -> empty ;

coherence
f ++ F is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster f ++ F -> non empty ;

coherence
not f ++ F is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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 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 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 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 ExtReal 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 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 holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)

proof end;

definition

let A be complex-membered set ;
let a be Complex;

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 holds a ++ A = {a} ++ A;

theorem Th141: :: MEMBER_1:141

for A being complex-membered set
for a, b being Complex 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 holds a ++ A = { (a + c) where c is Complex : c in A }

proof end;

theorem Th143: :: MEMBER_1:143

for A being complex-membered set
for a being Complex
for e being set st e in a ++ A holds
ex c being Complex st
( e = a + c & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster a ++ A -> empty ;

coherence
a ++ A is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster a ++ A -> non empty ;

coherence
not a ++ A is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster a ++ A -> complex-membered ;

coherence
a ++ A is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster a ++ A -> real-membered ;

coherence
a ++ A is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

cluster a ++ A -> rational-membered ;

coherence
a ++ A is rational-membered ;

end;

registration

let A be integer-membered set ;
let a be Integer;

cluster a ++ A -> integer-membered ;

coherence
a ++ A is integer-membered ;

end;

registration

let A be natural-membered set ;
let a be Nat;

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;
let f be ExtReal;

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 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 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 holds (a + b) ++ A = a ++ (b ++ A)

proof end;

theorem :: MEMBER_1:148

for A, B being complex-membered set
for a being Complex 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 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 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 holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)

proof end;

definition

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds f -- F = {f} -- F;

theorem Th152: :: MEMBER_1:152

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster f -- F -> empty ;

coherence
f -- F is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster f -- F -> non empty ;

coherence
not f -- F is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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 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 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 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 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 holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)

proof end;

definition

let A be complex-membered set ;
let a be Complex;

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 holds a -- A = {a} -- A;

theorem Th160: :: MEMBER_1:160

for A being complex-membered set
for a, b being Complex 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 holds a -- A = { (a - c) where c is Complex : c in A }

proof end;

theorem Th162: :: MEMBER_1:162

for A being complex-membered set
for a being Complex
for e being set st e in a -- A holds
ex c being Complex st
( e = a - c & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster a -- A -> empty ;

coherence
a -- A is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster a -- A -> non empty ;

coherence
not a -- A is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster a -- A -> complex-membered ;

coherence
a -- A is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster a -- A -> real-membered ;

coherence
a -- A is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

cluster a -- A -> rational-membered ;

coherence
a -- A is rational-membered ;

end;

registration

let A be integer-membered set ;
let a be Integer;

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;
let f be ExtReal;

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 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 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 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 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 holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)

proof end;

definition

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds F -- f = F -- {f};

theorem Th168: :: MEMBER_1:168

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster F -- f -> empty ;

coherence
F -- f is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster F -- f -> non empty ;

coherence
not F -- f is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds F -- f = -- (f -- F) by Th60;

theorem :: MEMBER_1:172

for F being ext-real-membered set
for f being ExtReal holds f -- F = -- (F -- f) by Th60;

theorem :: MEMBER_1:173

for F, G being ext-real-membered set
for r being Real 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 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 holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)

proof end;

definition

let A be complex-membered set ;
let a be Complex;

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 holds A -- a = A -- {a};

theorem Th176: :: MEMBER_1:176

for A being complex-membered set
for a, b being Complex 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 holds A -- a = { (c - a) where c is Complex : c in A }

proof end;

theorem Th178: :: MEMBER_1:178

for A being complex-membered set
for a being Complex
for e being set st e in A -- a holds
ex c being Complex st
( e = c - a & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster A -- a -> empty ;

coherence
A -- a is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster A -- a -> non empty ;

coherence
not A -- a is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster A -- a -> complex-membered ;

coherence
A -- a is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster A -- a -> real-membered ;

coherence
A -- a is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

cluster A -- a -> rational-membered ;

coherence
A -- a is rational-membered ;

end;

registration

let A be integer-membered set ;
let a be Integer;

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;
let f be ExtReal;

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 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 st A -- a = B -- a holds
A = B

proof end;

theorem :: MEMBER_1:181

for A being complex-membered set
for a being Complex holds A -- a = -- (a -- A) by Th71;

theorem :: MEMBER_1:182

for A being complex-membered set
for a being Complex holds a -- A = -- (A -- a) by Th71;

theorem :: MEMBER_1:183

for A, B being complex-membered set
for a being Complex 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 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 holds (A \+\ B) -- a = (A -- a) \+\ (B -- a)

proof end;

definition

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds f ** F = {f} ** F;

theorem Th186: :: MEMBER_1:186

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster f ** F -> empty ;

coherence
f ** F is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster f ** F -> non empty ;

coherence
not f ** F is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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 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 ExtReal 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 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 st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)

proof end;

definition

let A be complex-membered set ;
let a be Complex;

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 holds a ** A = {a} ** A;

theorem Th193: :: MEMBER_1:193

for A being complex-membered set
for a, b being Complex 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 holds a ** A = { (a * c) where c is Complex : c in A }

proof end;

theorem Th195: :: MEMBER_1:195

for A being complex-membered set
for a being Complex
for e being set st e in a ** A holds
ex c being Complex st
( e = a * c & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster a ** A -> empty ;

coherence
a ** A is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster a ** A -> non empty ;

coherence
not a ** A is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster a ** A -> complex-membered ;

coherence
a ** A is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster a ** A -> real-membered ;

coherence
a ** A is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

cluster a ** A -> rational-membered ;

coherence
a ** A is rational-membered ;

end;

registration

let A be integer-membered set ;
let a be Integer;

cluster a ** A -> integer-membered ;

coherence
a ** A is integer-membered ;

end;

registration

let A be natural-membered set ;
let a be Nat;

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;
let f be ExtReal;

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 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 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 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 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 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 holds (a * b) ** A = a ** (b ** A)

proof end;

theorem :: MEMBER_1:205

for A, B being complex-membered set
for a being Complex holds a ** (A ** B) = (a ** A) ** B by Th90;

theorem :: MEMBER_1:206

for A being complex-membered set
for a, b being Complex 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 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 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 holds a ** (B -- C) = (a ** B) -- (a ** C)

proof end;

definition

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds f /// F = {f} /// F;

theorem Th210: :: MEMBER_1:210

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster f /// F -> empty ;

coherence
f /// F is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster f /// F -> non empty ;

coherence
not f /// F is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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;

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 holds a /// A = {a} /// A;

theorem Th213: :: MEMBER_1:213

for A being complex-membered set
for a, b being Complex 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 holds a /// A = { (a / c) where c is Complex : c in A }

proof end;

theorem Th215: :: MEMBER_1:215

for A being complex-membered set
for a being Complex
for e being set st e in a /// A holds
ex c being Complex st
( e = a / c & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster a /// A -> empty ;

coherence
a /// A is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster a /// A -> non empty ;

coherence
not a /// A is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster a /// A -> complex-membered ;

coherence
a /// A is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster a /// A -> real-membered ;

coherence
a /// A is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

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;
let f be ExtReal;

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 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 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 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 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 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 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 holds (a - b) /// A c= (a /// A) -- (b /// A)

proof end;

definition

let F be ext-real-membered set ;
let f be ExtReal;

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 ExtReal holds F /// f = F /// {f};

theorem Th223: :: MEMBER_1:223

for G being ext-real-membered set
for f, g being ExtReal 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 ExtReal 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 ExtReal
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 ExtReal;

cluster F /// f -> empty ;

coherence
F /// f is empty ;

end;

registration

let F be ext-real-membered non empty set ;
let f be ExtReal;

cluster F /// f -> non empty ;

coherence
not F /// f is empty ;

end;

registration

let F be ext-real-membered set ;
let f be ExtReal;

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;

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 holds A /// a = A /// {a};

theorem Th226: :: MEMBER_1:226

for A being complex-membered set
for a, b being Complex 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 holds A /// a = { (c / a) where c is Complex : c in A }

proof end;

theorem Th228: :: MEMBER_1:228

for A being complex-membered set
for a being Complex
for e being set st e in A /// a holds
ex c being Complex st
( e = c / a & c in A )

proof end;

registration

let A be empty set ;
let a be Complex;

cluster A /// a -> empty ;

coherence
A /// a is empty ;

end;

registration

let A be complex-membered non empty set ;
let a be Complex;

cluster A /// a -> non empty ;

coherence
not A /// a is empty ;

end;

registration

let A be complex-membered set ;
let a be Complex;

cluster A /// a -> complex-membered ;

coherence
A /// a is complex-membered ;

end;

registration

let A be real-membered set ;
let a be Real;

cluster A /// a -> real-membered ;

coherence
A /// a is real-membered ;

end;

registration

let A be rational-membered set ;
let a be Rational;

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;
let f be ExtReal;

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 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 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 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 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 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 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 holds (A -- B) /// a = (A /// a) -- (B /// a)

proof end;