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

coherence

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

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

b_{2} = { (- c) where c is Complex : c in b_{1} }

end;
coherence

{ (- c) where c is 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 Complex : c in A } ;

for A being complex-membered set holds -- A = { (- c) where c is 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 ;

coherence

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

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

b_{2} = { (c ") where c is Complex : c in b_{1} }

end;
coherence

{ (c ") where c is 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 Complex : c in A } ;

for A being complex-membered set holds A "" = { (c ") where c is 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 ExtReal st f in F & g in G holds

f + g in F ++ G

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 ;

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 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 Complex : ( c1 in A & c2 in B ) } holds

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

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

{ (c1 + c2) where c1, c2 is 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 Complex : ( c1 in A & c2 in B ) } ;

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

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 ExtReal st f in F & g in G holds

f - g in F -- G

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 ;

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 Complex : ( c1 in A & c2 in 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 ExtReal st f in F & g in G holds

f * g in F ** G

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

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

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

{ (c1 * c2) where c1, c2 is 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 Complex : ( c1 in A & c2 in B ) } ;

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

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 ExtReal st f in F & g in G holds

f / g in F /// G

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 ;

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

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 ;

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

:: deftheorem defines ++ MEMBER_1:def 13 :

for F being ext-real-membered set

for f being ExtReal holds f ++ F = {f} ++ F;

for F being ext-real-membered set

for f being ExtReal holds f ++ F = {f} ++ F;

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 }

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 )

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

registration
end;

registration
end;

:: deftheorem defines ++ MEMBER_1:def 14 :

for A being complex-membered set

for a being Complex holds a ++ A = {a} ++ A;

for A being complex-membered set

for a being Complex holds a ++ A = {a} ++ A;

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

theorem :: MEMBER_1:148

theorem Th151: :: MEMBER_1:151

for A, B being complex-membered set

for a being Complex holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)

for a being Complex holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)

proof end;

:: deftheorem defines -- MEMBER_1:def 15 :

for F being ext-real-membered set

for f being ExtReal holds f -- F = {f} -- F;

for F being ext-real-membered set

for f being ExtReal holds f -- F = {f} -- F;

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 }

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 )

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

registration
end;

registration
end;

:: deftheorem defines -- MEMBER_1:def 16 :

for A being complex-membered set

for a being Complex holds a -- A = {a} -- A;

for A being complex-membered set

for a being Complex holds a -- A = {a} -- A;

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

theorem Th167: :: MEMBER_1:167

for A, B being complex-membered set

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

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

proof end;

:: deftheorem defines -- MEMBER_1:def 17 :

for F being ext-real-membered set

for f being ExtReal holds F -- f = F -- {f};

for F being ext-real-membered set

for f being ExtReal holds F -- f = F -- {f};

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 }

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 )

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

registration
end;

registration
end;

theorem :: MEMBER_1:171

theorem :: MEMBER_1:172

:: deftheorem defines -- MEMBER_1:def 18 :

for A being complex-membered set

for a being Complex holds A -- a = A -- {a};

for A being complex-membered set

for a being Complex holds A -- a = A -- {a};

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

theorem :: MEMBER_1:181

theorem :: MEMBER_1:182

theorem :: MEMBER_1:185

for A, B being complex-membered set

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

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

proof end;

:: deftheorem defines ** MEMBER_1:def 19 :

for F being ext-real-membered set

for f being ExtReal holds f ** F = {f} ** F;

for F being ext-real-membered set

for f being ExtReal holds f ** F = {f} ** F;

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 }

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 )

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

registration
end;

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

for r being Real st r <> 0 holds

r ** (F /\ G) = (r ** F) /\ (r ** 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)

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)

for r being Real st r <> 0 holds

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

proof end;

:: deftheorem defines ** MEMBER_1:def 20 :

for A being complex-membered set

for a being Complex holds a ** A = {a} ** A;

for A being complex-membered set

for a being Complex holds a ** A = {a} ** A;

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

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)

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)

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)

for a being Complex st a <> 0 holds

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

proof end;

theorem :: MEMBER_1:205

:: deftheorem defines /// MEMBER_1:def 21 :

for F being ext-real-membered set

for f being ExtReal holds f /// F = {f} /// F;

for F being ext-real-membered set

for f being ExtReal holds f /// F = {f} /// F;

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 }

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 )

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

registration
end;

registration
end;

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

for A being complex-membered set

for a being Complex holds a /// A = {a} /// A;

for A being complex-membered set

for a being Complex holds a /// A = {a} /// A;

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

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)

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)

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)

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)

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)

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

proof end;

:: deftheorem defines /// MEMBER_1:def 23 :

for F being ext-real-membered set

for f being ExtReal holds F /// f = F /// {f};

for F being ext-real-membered set

for f being ExtReal holds F /// f = F /// {f};

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 }

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 )

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

registration
end;

registration
end;

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

for A being complex-membered set

for a being Complex holds A /// a = A /// {a};

for A being complex-membered set

for a being Complex holds A /// a = A /// {a};

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 }

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 )

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

let f be ExtReal;

compatibility

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

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

let a be Real;

let f be ExtReal;

compatibility

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

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)

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)

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)

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)

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)

for a being Complex holds (A -- B) /// a = (A /// a) -- (B /// a)

proof end;