:: by Artur Korni{\l}owicz

::

:: Received December 19, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

definition

let w be Element of ExtREAL ;

:: original: -

redefine func - w -> Element of ExtREAL ;

coherence

- w is Element of ExtREAL by XXREAL_0:def 1;

:: original: "

redefine 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;
:: 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;

registration
end;

registration
end;

definition

let F be ext-real-membered set ;

{ (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set

for b_{1}, b_{2} being ext-real-membered set st b_{1} = { (- w) where w is Element of ExtREAL : w in b_{2} } holds

b_{2} = { (- w) where w is Element of ExtREAL : w in b_{1} }

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

{ (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set

proof end;

involutiveness for b

b

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

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

registration
end;

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

-- F c= -- G

proof end;

definition

let A be complex-membered set ;

{ (- c) where c is Element of COMPLEX : c in A } is complex-membered set

for b_{1}, b_{2} being complex-membered set st b_{1} = { (- c) where c is Element of COMPLEX : c in b_{2} } holds

b_{2} = { (- c) where c is Element of COMPLEX : c in b_{1} }

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

{ (- c) where c is Element of COMPLEX : c in A } is complex-membered set

proof end;

involutiveness for b

b

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

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

registration
end;

registration

let A be real-membered set ;

let F be ext-real-membered set ;

compatibility

( A = F implies -- A = -- F )

end;
let F be ext-real-membered set ;

compatibility

( A = F implies -- A = -- F )

proof end;

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

-- A c= -- B

proof end;

definition

let F be ext-real-membered set ;

{ (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set

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

{ (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set

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

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

registration
end;

definition

let A be complex-membered set ;

{ (c ") where c is Element of COMPLEX : c in A } is complex-membered set

for b_{1}, b_{2} being complex-membered set st b_{1} = { (c ") where c is Element of COMPLEX : c in b_{2} } holds

b_{2} = { (c ") where c is Element of COMPLEX : c in b_{1} }

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

{ (c ") where c is Element of COMPLEX : c in A } is complex-membered set

proof end;

involutiveness for b

b

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

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

registration
end;

registration

let A be real-membered set ;

let F be ext-real-membered set ;

compatibility

( A = F implies A "" = F "" )

end;
let F be ext-real-membered set ;

compatibility

( A = F implies A "" = F "" )

proof end;

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

A "" c= B ""

proof end;

definition

let F, G be ext-real-membered set ;

{ (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;

commutativity

for b_{1} being set

for F, G being ext-real-membered set st b_{1} = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds

b_{1} = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }

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

{ (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;

commutativity

for b

for F, G being ext-real-membered set st b

b

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

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

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 ;

coherence

F ++ G is empty

G ++ F is empty ;

end;
let G be ext-real-membered set ;

coherence

F ++ G is empty

proof end;

coherence G ++ F is empty ;

registration
end;

registration
end;

definition

let A, B be complex-membered set ;

{ (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;

commutativity

for b_{1} being set

for A, B being complex-membered set st b_{1} = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds

b_{1} = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }

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

{ (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;

commutativity

for b

for A, B being complex-membered set st b

b

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

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

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 ;

coherence

A ++ B is empty

B ++ A is empty ;

end;
let B be complex-membered set ;

coherence

A ++ B is empty

proof end;

coherence B ++ A is empty ;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let A, B be real-membered set ;

let F, G be ext-real-membered set ;

compatibility

( A = F & B = G implies A ++ B = F ++ G )

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

compatibility

( A = F & B = G implies A ++ B = F ++ G )

proof end;

:: deftheorem defines -- MEMBER_1:def 7 :

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

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

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 ;

coherence

F -- G is empty ;

coherence

G -- F is empty ;

end;
let G be ext-real-membered set ;

coherence

F -- G is empty ;

coherence

G -- F is empty ;

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

proof end;

:: deftheorem defines -- MEMBER_1:def 8 :

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

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

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 ;

coherence

A -- B is empty ;

coherence

B -- A is empty ;

end;
let B be complex-membered set ;

coherence

A -- B is empty ;

coherence

B -- A is empty ;

registration

let A, B be real-membered set ;

let F, G be ext-real-membered set ;

compatibility

( A = F & B = G implies A -- B = F -- G ) ;

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

compatibility

( A = F & B = G implies A -- B = F -- G ) ;

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

proof end;

theorem :: MEMBER_1:72

definition

let F, G be ext-real-membered set ;

{ (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;

commutativity

for b_{1} being set

for F, G being ext-real-membered set st b_{1} = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds

b_{1} = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }

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

{ (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;

commutativity

for b

for F, G being ext-real-membered set st b

b

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

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 ;

coherence

F ** G is empty

G ** F is empty ;

end;
let G be ext-real-membered set ;

coherence

F ** G is empty

proof end;

coherence G ** F is empty ;

registration
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

for f, g being ext-real number st f in F & g in G holds

f * g in F ** G

proof end;

registration
end;

definition

let A, B be complex-membered set ;

{ (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;

commutativity

for b_{1} being set

for A, B being complex-membered set st b_{1} = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds

b_{1} = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }

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

{ (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;

commutativity

for b

for A, B being complex-membered set st b

b

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

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

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 ;

coherence

A ** B is empty

B ** A is empty ;

end;
let B be complex-membered set ;

coherence

A ** B is empty

proof end;

coherence B ** A is empty ;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let A, B be real-membered set ;

let F, G be ext-real-membered set ;

compatibility

( A = F & B = G implies A ** B = F ** G )

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

compatibility

( A = F & B = G implies A ** B = F ** G )

proof end;

:: deftheorem defines /// MEMBER_1:def 11 :

for F, G being ext-real-membered set holds F /// G = F ** (G "");

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

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 ;

coherence

F /// G is empty ;

coherence

G /// F is empty ;

end;
let G be ext-real-membered set ;

coherence

F /// G is empty ;

coherence

G /// F is empty ;

theorem :: MEMBER_1:104

theorem :: MEMBER_1:105

theorem :: MEMBER_1:108

theorem :: MEMBER_1:109

:: deftheorem defines /// MEMBER_1:def 12 :

for A, B being complex-membered set holds A /// B = A ** (B "");

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

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 ;

coherence

A /// B is empty ;

coherence

B /// A is empty ;

end;
let B be complex-membered set ;

coherence

A /// B is empty ;

coherence

B /// A is empty ;

registration

let A, B be real-membered set ;

let F, G be ext-real-membered set ;

compatibility

( A = F & B = G implies A /// B = F /// G ) ;

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

compatibility

( A = F & B = G implies A /// B = F /// G ) ;

theorem :: MEMBER_1:121

theorem :: MEMBER_1:122

theorem :: MEMBER_1:124

theorem :: MEMBER_1:125

definition
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;

for F being ext-real-membered set

for f being ext-real number holds f ++ F = {f} ++ F;

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not f ++ F is empty ;

end;
let f be ext-real number ;

coherence

not f ++ F is empty ;

registration
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)

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)

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)

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)

for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)

proof end;

definition
end;

:: deftheorem defines ++ MEMBER_1:def 14 :

for A being complex-membered set

for a being complex number holds a ++ A = {a} ++ A;

for A being complex-membered set

for a being complex number holds a ++ A = {a} ++ A;

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 }

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 )

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

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies a ++ A = f ++ F ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies a ++ A = f ++ F ) ;

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 )

for a being complex number holds

( A c= B iff a ++ A c= a ++ B )

proof end;

theorem :: MEMBER_1:148

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)

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)

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)

for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)

proof end;

definition
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;

for F being ext-real-membered set

for f being ext-real number holds f -- F = {f} -- F;

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not f -- F is empty ;

end;
let f be ext-real number ;

coherence

not f -- F is empty ;

registration
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)

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)

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)

for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)

proof end;

definition
end;

:: deftheorem defines -- MEMBER_1:def 16 :

for A being complex-membered set

for a being complex number holds a -- A = {a} -- A;

for A being complex-membered set

for a being complex number holds a -- A = {a} -- A;

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 }

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 )

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

registration
end;

registration
end;

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies a -- A = f -- F ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies a -- A = f -- F ) ;

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 )

for a being complex number holds

( A c= B iff a -- A c= 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)

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)

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)

for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)

proof end;

definition
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};

for F being ext-real-membered set

for f being ext-real number holds F -- f = F -- {f};

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not F -- f is empty ;

end;
let f be ext-real number ;

coherence

not F -- f is empty ;

registration
end;

theorem :: MEMBER_1:171

theorem :: MEMBER_1:172

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)

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)

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)

for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)

proof end;

definition
end;

:: deftheorem defines -- MEMBER_1:def 18 :

for A being complex-membered set

for a being complex number holds A -- a = A -- {a};

for A being complex-membered set

for a being complex number holds A -- a = A -- {a};

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 }

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 )

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

registration
end;

registration
end;

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies A -- a = F -- f ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies A -- a = F -- f ) ;

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 )

for a being complex number holds

( A c= B iff A -- a c= B -- a )

proof end;

theorem :: MEMBER_1:181

theorem :: MEMBER_1:182

theorem :: MEMBER_1:183

for A, B being complex-membered set

for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a)

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)

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)

for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a)

proof end;

definition
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;

for F being ext-real-membered set

for f being ext-real number holds f ** F = {f} ** F;

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not f ** F is empty ;

end;
let f be ext-real number ;

coherence

not f ** F is empty ;

registration
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)

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)

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)

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)

for r being real number st r <> 0 holds

r ** (F \+\ G) = (r ** F) \+\ (r ** G)

proof end;

definition
end;

:: deftheorem defines ** MEMBER_1:def 20 :

for A being complex-membered set

for a being complex number holds a ** A = {a} ** A;

for A being complex-membered set

for a being complex number holds a ** A = {a} ** A;

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 }

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 )

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

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies a ** A = f ** F ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies a ** A = f ** F ) ;

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

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

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)

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)

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)

for a being complex number st a <> 0 holds

a ** (A \+\ B) = (a ** A) \+\ (a ** B)

proof end;

theorem :: MEMBER_1:205

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)

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)

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)

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)

for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C)

proof end;

definition
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;

for F being ext-real-membered set

for f being ext-real number holds f /// F = {f} /// F;

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not f /// F is empty ;

end;
let f be ext-real number ;

coherence

not f /// F is empty ;

registration
end;

definition
end;

:: deftheorem defines /// MEMBER_1:def 22 :

for A being complex-membered set

for a being complex number holds a /// A = {a} /// A;

for A being complex-membered set

for a being complex number holds a /// A = {a} /// A;

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 }

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 )

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

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies a /// A = f /// F ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies a /// A = f /// F ) ;

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

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

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)

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)

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)

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)

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)

for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A)

proof end;

definition
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};

for F being ext-real-membered set

for f being ext-real number holds F /// f = F /// {f};

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 }

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 )

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 non empty ext-real-membered set ;

let f be ext-real number ;

coherence

not F /// f is empty ;

end;
let f be ext-real number ;

coherence

not F /// f is empty ;

registration
end;

definition
end;

:: deftheorem defines /// MEMBER_1:def 24 :

for A being complex-membered set

for a being complex number holds A /// a = A /// {a};

for A being complex-membered set

for a being complex number holds A /// a = A /// {a};

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 }

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 )

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

registration
end;

registration
end;

registration
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 ;

compatibility

( A = F & a = f implies A /// a = F /// f ) ;

end;
let F be ext-real-membered set ;

let a be real number ;

let f be ext-real number ;

compatibility

( A = F & a = f implies A /// a = F /// f ) ;

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

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

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)

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)

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)

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)

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)

for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a)

proof end;