:: MEMBER_1 semantic presentation begin definition let w be Element of ExtREAL ; :: original: - redefine func - w -> Element of ExtREAL ; coherence - w is Element of ExtREAL by XXREAL_0:def_1; :: original: " redefine funcw " -> Element of ExtREAL ; coherence w " is Element of ExtREAL by XXREAL_0:def_1; let w1 be Element of ExtREAL ; :: original: * redefine funcw * w1 -> Element of ExtREAL ; coherence w * w1 is Element of ExtREAL by XXREAL_0:def_1; end; registration let a, b, c, d be complex number ; cluster{a,b,c,d} -> complex-membered ; coherence {a,b,c,d} is complex-membered proof let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in {a,b,c,d} or e is complex ) thus ( not e in {a,b,c,d} or e is complex ) by ENUMSET1:def_2; ::_thesis: verum end; end; registration let a, b, c, d be ext-real number ; cluster{a,b,c,d} -> ext-real-membered ; coherence {a,b,c,d} is ext-real-membered proof let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in {a,b,c,d} or e is ext-real ) thus ( not e in {a,b,c,d} or e is ext-real ) by ENUMSET1:def_2; ::_thesis: verum end; end; definition let F be ext-real-membered set ; func -- F -> ext-real-membered set equals :: MEMBER_1:def 1 { (- w) where w is Element of ExtREAL : w in F } ; coherence { (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set proof { (- w) where w is Element of ExtREAL : w in F } is ext-real-membered proof let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in { (- w) where w is Element of ExtREAL : w in F } or e is ext-real ) assume e in { (- w) where w is Element of ExtREAL : w in F } ; ::_thesis: e is ext-real then ex w being Element of ExtREAL st ( e = - w & w in F ) ; hence e is ext-real ; ::_thesis: verum end; hence { (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set ; ::_thesis: verum end; involutiveness for b1, b2 being ext-real-membered set st b1 = { (- w) where w is Element of ExtREAL : w in b2 } holds b2 = { (- w) where w is Element of ExtREAL : w in b1 } proof let A, B be ext-real-membered set ; ::_thesis: ( A = { (- w) where w is Element of ExtREAL : w in B } implies B = { (- w) where w is Element of ExtREAL : w in A } ) assume A1: A = { (- w) where w is Element of ExtREAL : w in B } ; ::_thesis: B = { (- w) where w is Element of ExtREAL : w in A } thus B c= { (- w) where w is Element of ExtREAL : w in A } :: according to XBOOLE_0:def_10 ::_thesis: { (- w) where w is Element of ExtREAL : w in A } c= B proof let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in B or z in { (- w) where w is Element of ExtREAL : w in A } ) A2: z in ExtREAL by XXREAL_0:def_1; A3: ( - z in ExtREAL & z = - (- z) ) by XXREAL_0:def_1; assume z in B ; ::_thesis: z in { (- w) where w is Element of ExtREAL : w in A } then - z in A by A1, A2; hence z in { (- w) where w is Element of ExtREAL : w in A } by A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (- w) where w is Element of ExtREAL : w in A } or e in B ) assume e in { (- w) where w is Element of ExtREAL : w in A } ; ::_thesis: e in B then consider w1 being Element of ExtREAL such that A4: - w1 = e and A5: w1 in A ; ex w being Element of ExtREAL st ( - w = w1 & w in B ) by A1, A5; hence e in B by A4; ::_thesis: verum end; end; :: deftheorem defines -- MEMBER_1:def_1_:_ for F being ext-real-membered set holds -- F = { (- w) where w is Element of ExtREAL : w in F } ; theorem Th1: :: MEMBER_1:1 for F being ext-real-membered set for f being ext-real number holds ( f in F iff - f in -- F ) proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds ( f in F iff - f in -- F ) let f be ext-real number ; ::_thesis: ( f in F iff - f in -- F ) f in ExtREAL by XXREAL_0:def_1; hence ( f in F implies - f in -- F ) ; ::_thesis: ( - f in -- F implies f in F ) assume - f in -- F ; ::_thesis: f in F then A1: ex w being Element of ExtREAL st ( - w = - f & w in F ) ; - (- f) = f ; hence f in F by A1; ::_thesis: verum end; theorem Th2: :: MEMBER_1:2 for F being ext-real-membered set for f being ext-real number holds ( - f in F iff f in -- F ) proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds ( - f in F iff f in -- F ) let f be ext-real number ; ::_thesis: ( - f in F iff f in -- F ) - (- f) = f ; hence ( - f in F iff f in -- F ) by Th1; ::_thesis: verum end; registration let F be empty set ; cluster -- F -> empty ext-real-membered ; coherence -- F is empty proof assume not -- F is empty ; ::_thesis: contradiction then the Element of -- F in -- F ; then ex w being Element of ExtREAL st ( the Element of -- F = - w & w in F ) ; hence contradiction ; ::_thesis: verum end; end; registration let F be non empty ext-real-membered set ; cluster -- F -> non empty ext-real-membered ; coherence not -- F is empty proof - the Element of F in -- F by Th1; hence not -- F is empty ; ::_thesis: verum end; end; Lm1: for F, G being ext-real-membered set st F c= G holds -- F c= -- G proof let F, G be ext-real-membered set ; ::_thesis: ( F c= G implies -- F c= -- G ) assume A1: F c= G ; ::_thesis: -- F c= -- G let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in -- F or j in -- G ) assume j in -- F ; ::_thesis: j in -- G then - j in F by Th2; hence j in -- G by A1, Th2; ::_thesis: verum end; theorem Th3: :: MEMBER_1:3 for F, G being ext-real-membered set holds ( F c= G iff -- F c= -- G ) proof let F, G be ext-real-membered set ; ::_thesis: ( F c= G iff -- F c= -- G ) ( -- (-- F) = F & -- (-- G) = G ) ; hence ( F c= G iff -- F c= -- G ) by Lm1; ::_thesis: verum end; theorem :: MEMBER_1:4 for F, G being ext-real-membered set st -- F = -- G holds F = G proof let F, G be ext-real-membered set ; ::_thesis: ( -- F = -- G implies F = G ) assume -- F = -- G ; ::_thesis: F = G then ( F c= G & G c= F ) by Th3; hence F = G by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th5: :: MEMBER_1:5 for F, G being ext-real-membered set holds -- (F \/ G) = (-- F) \/ (-- G) proof let F, G be ext-real-membered set ; ::_thesis: -- (F \/ G) = (-- F) \/ (-- G) let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F \/ G) or i in (-- F) \/ (-- G) ) & ( not i in (-- F) \/ (-- G) or i in -- (F \/ G) ) ) hereby ::_thesis: ( not i in (-- F) \/ (-- G) or i in -- (F \/ G) ) assume i in -- (F \/ G) ; ::_thesis: i in (-- F) \/ (-- G) then - i in F \/ G by Th2; then ( - i in F or - i in G ) by XBOOLE_0:def_3; then ( i in -- F or i in -- G ) by Th2; hence i in (-- F) \/ (-- G) by XBOOLE_0:def_3; ::_thesis: verum end; assume i in (-- F) \/ (-- G) ; ::_thesis: i in -- (F \/ G) then ( i in -- F or i in -- G ) by XBOOLE_0:def_3; then ( - i in F or - i in G ) by Th2; then - i in F \/ G by XBOOLE_0:def_3; hence i in -- (F \/ G) by Th2; ::_thesis: verum end; theorem Th6: :: MEMBER_1:6 for F, G being ext-real-membered set holds -- (F /\ G) = (-- F) /\ (-- G) proof let F, G be ext-real-membered set ; ::_thesis: -- (F /\ G) = (-- F) /\ (-- G) let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F /\ G) or i in (-- F) /\ (-- G) ) & ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) ) ) hereby ::_thesis: ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) ) assume i in -- (F /\ G) ; ::_thesis: i in (-- F) /\ (-- G) then A1: - i in F /\ G by Th2; then - i in G by XBOOLE_0:def_4; then A2: i in -- G by Th2; - i in F by A1, XBOOLE_0:def_4; then i in -- F by Th2; hence i in (-- F) /\ (-- G) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: i in (-- F) /\ (-- G) ; ::_thesis: i in -- (F /\ G) then i in -- G by XBOOLE_0:def_4; then A4: - i in G by Th2; i in -- F by A3, XBOOLE_0:def_4; then - i in F by Th2; then - i in F /\ G by A4, XBOOLE_0:def_4; hence i in -- (F /\ G) by Th2; ::_thesis: verum end; theorem Th7: :: MEMBER_1:7 for F, G being ext-real-membered set holds -- (F \ G) = (-- F) \ (-- G) proof let F, G be ext-real-membered set ; ::_thesis: -- (F \ G) = (-- F) \ (-- G) let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F \ G) or i in (-- F) \ (-- G) ) & ( not i in (-- F) \ (-- G) or i in -- (F \ G) ) ) hereby ::_thesis: ( not i in (-- F) \ (-- G) or i in -- (F \ G) ) assume i in -- (F \ G) ; ::_thesis: i in (-- F) \ (-- G) then A1: - i in F \ G by Th2; then not - i in G by XBOOLE_0:def_5; then A2: not i in -- G by Th2; i in -- F by A1, Th2; hence i in (-- F) \ (-- G) by A2, XBOOLE_0:def_5; ::_thesis: verum end; assume A3: i in (-- F) \ (-- G) ; ::_thesis: i in -- (F \ G) then not i in -- G by XBOOLE_0:def_5; then A4: not - i in G by Th2; - i in F by A3, Th2; then - i in F \ G by A4, XBOOLE_0:def_5; hence i in -- (F \ G) by Th2; ::_thesis: verum end; theorem Th8: :: MEMBER_1:8 for F, G being ext-real-membered set holds -- (F \+\ G) = (-- F) \+\ (-- G) proof let F, G be ext-real-membered set ; ::_thesis: -- (F \+\ G) = (-- F) \+\ (-- G) thus -- (F \+\ G) = (-- (F \ G)) \/ (-- (G \ F)) by Th5 .= ((-- F) \ (-- G)) \/ (-- (G \ F)) by Th7 .= (-- F) \+\ (-- G) by Th7 ; ::_thesis: verum end; theorem Th9: :: MEMBER_1:9 for f being ext-real number holds -- {f} = {(- f)} proof let f be ext-real number ; ::_thesis: -- {f} = {(- f)} let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- {f} or i in {(- f)} ) & ( not i in {(- f)} or i in -- {f} ) ) hereby ::_thesis: ( not i in {(- f)} or i in -- {f} ) assume i in -- {f} ; ::_thesis: i in {(- f)} then consider w being Element of ExtREAL such that A1: i = - w and A2: w in {f} ; w = f by A2, TARSKI:def_1; hence i in {(- f)} by A1, TARSKI:def_1; ::_thesis: verum end; assume i in {(- f)} ; ::_thesis: i in -- {f} then A3: i = - f by TARSKI:def_1; ( f in ExtREAL & f in {f} ) by TARSKI:def_1, XXREAL_0:def_1; hence i in -- {f} by A3; ::_thesis: verum end; theorem Th10: :: MEMBER_1:10 for f, g being ext-real number holds -- {f,g} = {(- f),(- g)} proof let f, g be ext-real number ; ::_thesis: -- {f,g} = {(- f),(- g)} thus -- {f,g} = -- ({f} \/ {g}) by ENUMSET1:1 .= (-- {f}) \/ (-- {g}) by Th5 .= {(- f)} \/ (-- {g}) by Th9 .= {(- f)} \/ {(- g)} by Th9 .= {(- f),(- g)} by ENUMSET1:1 ; ::_thesis: verum end; definition let A be complex-membered set ; func -- A -> complex-membered set equals :: MEMBER_1:def 2 { (- c) where c is Element of COMPLEX : c in A } ; coherence { (- c) where c is Element of COMPLEX : c in A } is complex-membered set proof { (- c) where c is Element of COMPLEX : c in A } is complex-membered proof let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in { (- c) where c is Element of COMPLEX : c in A } or e is complex ) assume e in { (- c) where c is Element of COMPLEX : c in A } ; ::_thesis: e is complex then ex c being Element of COMPLEX st ( e = - c & c in A ) ; hence e is complex ; ::_thesis: verum end; hence { (- c) where c is Element of COMPLEX : c in A } is complex-membered set ; ::_thesis: verum end; involutiveness for b1, b2 being complex-membered set st b1 = { (- c) where c is Element of COMPLEX : c in b2 } holds b2 = { (- c) where c is Element of COMPLEX : c in b1 } proof let A, B be complex-membered set ; ::_thesis: ( A = { (- c) where c is Element of COMPLEX : c in B } implies B = { (- c) where c is Element of COMPLEX : c in A } ) assume A1: A = { (- c) where c is Element of COMPLEX : c in B } ; ::_thesis: B = { (- c) where c is Element of COMPLEX : c in A } thus B c= { (- c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (- c) where c is Element of COMPLEX : c in A } c= B proof let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in B or z in { (- c) where c is Element of COMPLEX : c in A } ) A2: z in COMPLEX by XCMPLX_0:def_2; A3: ( - z in COMPLEX & z = - (- z) ) by XCMPLX_0:def_2; assume z in B ; ::_thesis: z in { (- c) where c is Element of COMPLEX : c in A } then - z in A by A1, A2; hence z in { (- c) where c is Element of COMPLEX : c in A } by A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (- c) where c is Element of COMPLEX : c in A } or e in B ) assume e in { (- c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in B then consider r0 being Element of COMPLEX such that A4: - r0 = e and A5: r0 in A ; ex c being Element of COMPLEX st ( - c = r0 & c in B ) by A1, A5; hence e in B by A4; ::_thesis: verum end; end; :: deftheorem defines -- MEMBER_1:def_2_:_ for A being complex-membered set holds -- A = { (- c) where c is Element of COMPLEX : c in A } ; theorem Th11: :: MEMBER_1:11 for A being complex-membered set for a being complex number holds ( a in A iff - a in -- A ) proof let A be complex-membered set ; ::_thesis: for a being complex number holds ( a in A iff - a in -- A ) let a be complex number ; ::_thesis: ( a in A iff - a in -- A ) a in COMPLEX by XCMPLX_0:def_2; hence ( a in A implies - a in -- A ) ; ::_thesis: ( - a in -- A implies a in A ) assume - a in -- A ; ::_thesis: a in A then ex c being Element of COMPLEX st ( - c = - a & c in A ) ; hence a in A ; ::_thesis: verum end; theorem Th12: :: MEMBER_1:12 for A being complex-membered set for a being complex number holds ( - a in A iff a in -- A ) proof let A be complex-membered set ; ::_thesis: for a being complex number holds ( - a in A iff a in -- A ) let a be complex number ; ::_thesis: ( - a in A iff a in -- A ) - (- a) = a ; hence ( - a in A iff a in -- A ) by Th11; ::_thesis: verum end; registration let A be empty set ; cluster -- A -> empty complex-membered ; coherence -- A is empty proof assume not -- A is empty ; ::_thesis: contradiction then the Element of -- A in -- A ; then ex c being Element of COMPLEX st ( the Element of -- A = - c & c in A ) ; hence contradiction ; ::_thesis: verum end; end; registration let A be non empty complex-membered set ; cluster -- A -> non empty complex-membered ; coherence not -- A is empty proof - the Element of A in -- A by Th11; hence not -- A is empty ; ::_thesis: verum end; end; registration let A be real-membered set ; cluster -- A -> complex-membered real-membered ; coherence -- A is real-membered proof let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in -- A or e is real ) assume e in -- A ; ::_thesis: e is real then ex c being Element of COMPLEX st ( e = - c & c in A ) ; hence e is real ; ::_thesis: verum end; end; registration let A be rational-membered set ; cluster -- A -> complex-membered rational-membered ; coherence -- A is rational-membered proof let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in -- A or e is rational ) assume e in -- A ; ::_thesis: e is rational then ex c being Element of COMPLEX st ( e = - c & c in A ) ; hence e is rational ; ::_thesis: verum end; end; registration let A be integer-membered set ; cluster -- A -> complex-membered integer-membered ; coherence -- A is integer-membered proof let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in -- A or e is integer ) assume e in -- A ; ::_thesis: e is integer then ex c being Element of COMPLEX st ( e = - c & c in A ) ; hence e is integer ; ::_thesis: verum 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 assume A1: A = F ; ::_thesis: -- A = -- F let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in -- A or a in -- F ) & ( not a in -- F or a in -- A ) ) hereby ::_thesis: ( not a in -- F or a in -- A ) assume A2: a in -- A ; ::_thesis: a in -- F then reconsider b = a as real number ; - b in A by A2, Th12; hence a in -- F by A1, Th2; ::_thesis: verum end; assume a in -- F ; ::_thesis: a in -- A then consider w being Element of ExtREAL such that A3: a = - w and A4: w in F ; reconsider b = w as real number by A1, A4; - b in COMPLEX by XCMPLX_0:def_2; then - a in COMPLEX by A3, XCMPLX_0:def_2; then - b in -- A by A1, A3, A4; hence a in -- A by A3; ::_thesis: verum end; end; Lm2: for A, B being complex-membered set st A c= B holds -- A c= -- B proof let A, B be complex-membered set ; ::_thesis: ( A c= B implies -- A c= -- B ) assume A1: A c= B ; ::_thesis: -- A c= -- B let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in -- A or a in -- B ) assume a in -- A ; ::_thesis: a in -- B then - a in A by Th12; hence a in -- B by A1, Th12; ::_thesis: verum end; theorem Th13: :: MEMBER_1:13 for A, B being complex-membered set holds ( A c= B iff -- A c= -- B ) proof let A, B be complex-membered set ; ::_thesis: ( A c= B iff -- A c= -- B ) ( -- (-- A) = A & -- (-- B) = B ) ; hence ( A c= B iff -- A c= -- B ) by Lm2; ::_thesis: verum end; theorem :: MEMBER_1:14 for A, B being complex-membered set st -- A = -- B holds A = B proof let A, B be complex-membered set ; ::_thesis: ( -- A = -- B implies A = B ) assume -- A = -- B ; ::_thesis: A = B then ( A c= B & B c= A ) by Th13; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th15: :: MEMBER_1:15 for A, B being complex-membered set holds -- (A \/ B) = (-- A) \/ (-- B) proof let A, B be complex-membered set ; ::_thesis: -- (A \/ B) = (-- A) \/ (-- B) let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A \/ B) or z in (-- A) \/ (-- B) ) & ( not z in (-- A) \/ (-- B) or z in -- (A \/ B) ) ) hereby ::_thesis: ( not z in (-- A) \/ (-- B) or z in -- (A \/ B) ) assume z in -- (A \/ B) ; ::_thesis: z in (-- A) \/ (-- B) then - z in A \/ B by Th12; then ( - z in A or - z in B ) by XBOOLE_0:def_3; then ( z in -- A or z in -- B ) by Th12; hence z in (-- A) \/ (-- B) by XBOOLE_0:def_3; ::_thesis: verum end; assume z in (-- A) \/ (-- B) ; ::_thesis: z in -- (A \/ B) then ( z in -- A or z in -- B ) by XBOOLE_0:def_3; then ( - z in A or - z in B ) by Th12; then - z in A \/ B by XBOOLE_0:def_3; hence z in -- (A \/ B) by Th12; ::_thesis: verum end; theorem Th16: :: MEMBER_1:16 for A, B being complex-membered set holds -- (A /\ B) = (-- A) /\ (-- B) proof let A, B be complex-membered set ; ::_thesis: -- (A /\ B) = (-- A) /\ (-- B) let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A /\ B) or z in (-- A) /\ (-- B) ) & ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) ) ) hereby ::_thesis: ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) ) assume z in -- (A /\ B) ; ::_thesis: z in (-- A) /\ (-- B) then A1: - z in A /\ B by Th12; then - z in B by XBOOLE_0:def_4; then A2: z in -- B by Th12; - z in A by A1, XBOOLE_0:def_4; then z in -- A by Th12; hence z in (-- A) /\ (-- B) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: z in (-- A) /\ (-- B) ; ::_thesis: z in -- (A /\ B) then z in -- B by XBOOLE_0:def_4; then A4: - z in B by Th12; z in -- A by A3, XBOOLE_0:def_4; then - z in A by Th12; then - z in A /\ B by A4, XBOOLE_0:def_4; hence z in -- (A /\ B) by Th12; ::_thesis: verum end; theorem Th17: :: MEMBER_1:17 for A, B being complex-membered set holds -- (A \ B) = (-- A) \ (-- B) proof let A, B be complex-membered set ; ::_thesis: -- (A \ B) = (-- A) \ (-- B) let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A \ B) or z in (-- A) \ (-- B) ) & ( not z in (-- A) \ (-- B) or z in -- (A \ B) ) ) hereby ::_thesis: ( not z in (-- A) \ (-- B) or z in -- (A \ B) ) assume z in -- (A \ B) ; ::_thesis: z in (-- A) \ (-- B) then A1: - z in A \ B by Th12; then not - z in B by XBOOLE_0:def_5; then A2: not z in -- B by Th12; z in -- A by A1, Th12; hence z in (-- A) \ (-- B) by A2, XBOOLE_0:def_5; ::_thesis: verum end; assume A3: z in (-- A) \ (-- B) ; ::_thesis: z in -- (A \ B) then not z in -- B by XBOOLE_0:def_5; then A4: not - z in B by Th12; - z in A by A3, Th12; then - z in A \ B by A4, XBOOLE_0:def_5; hence z in -- (A \ B) by Th12; ::_thesis: verum end; theorem Th18: :: MEMBER_1:18 for A, B being complex-membered set holds -- (A \+\ B) = (-- A) \+\ (-- B) proof let A, B be complex-membered set ; ::_thesis: -- (A \+\ B) = (-- A) \+\ (-- B) thus -- (A \+\ B) = (-- (A \ B)) \/ (-- (B \ A)) by Th15 .= ((-- A) \ (-- B)) \/ (-- (B \ A)) by Th17 .= (-- A) \+\ (-- B) by Th17 ; ::_thesis: verum end; theorem Th19: :: MEMBER_1:19 for a being complex number holds -- {a} = {(- a)} proof let a be complex number ; ::_thesis: -- {a} = {(- a)} let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- {a} or z in {(- a)} ) & ( not z in {(- a)} or z in -- {a} ) ) hereby ::_thesis: ( not z in {(- a)} or z in -- {a} ) assume z in -- {a} ; ::_thesis: z in {(- a)} then consider c being Element of COMPLEX such that A1: z = - c and A2: c in {a} ; c = a by A2, TARSKI:def_1; hence z in {(- a)} by A1, TARSKI:def_1; ::_thesis: verum end; assume z in {(- a)} ; ::_thesis: z in -- {a} then A3: z = - a by TARSKI:def_1; ( a in COMPLEX & a in {a} ) by TARSKI:def_1, XCMPLX_0:def_2; hence z in -- {a} by A3; ::_thesis: verum end; theorem Th20: :: MEMBER_1:20 for a, b being complex number holds -- {a,b} = {(- a),(- b)} proof let a, b be complex number ; ::_thesis: -- {a,b} = {(- a),(- b)} thus -- {a,b} = -- ({a} \/ {b}) by ENUMSET1:1 .= (-- {a}) \/ (-- {b}) by Th15 .= {(- a)} \/ (-- {b}) by Th19 .= {(- a)} \/ {(- b)} by Th19 .= {(- a),(- b)} by ENUMSET1:1 ; ::_thesis: verum end; definition let F be ext-real-membered set ; funcF "" -> ext-real-membered set equals :: MEMBER_1:def 3 { (w ") where w is Element of ExtREAL : w in F } ; coherence { (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set proof { (w ") where w is Element of ExtREAL : w in F } is ext-real-membered proof let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in { (w ") where w is Element of ExtREAL : w in F } or e is ext-real ) assume e in { (w ") where w is Element of ExtREAL : w in F } ; ::_thesis: e is ext-real then ex w being Element of ExtREAL st ( e = w " & w in F ) ; hence e is ext-real ; ::_thesis: verum end; hence { (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set ; ::_thesis: verum end; end; :: deftheorem defines "" MEMBER_1:def_3_:_ for F being ext-real-membered set holds F "" = { (w ") where w is Element of ExtREAL : w in F } ; theorem Th21: :: MEMBER_1:21 for F being ext-real-membered set for f being ext-real number st f in F holds f " in F "" proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number st f in F holds f " in F "" let f be ext-real number ; ::_thesis: ( f in F implies f " in F "" ) f in ExtREAL by XXREAL_0:def_1; hence ( f in F implies f " in F "" ) ; ::_thesis: verum end; registration let F be empty set ; clusterF "" -> empty ext-real-membered ; coherence F "" is empty proof assume not F "" is empty ; ::_thesis: contradiction then the Element of F "" in F "" ; then ex w being Element of ExtREAL st ( the Element of F "" = w " & w in F ) ; hence contradiction ; ::_thesis: verum end; end; registration let F be non empty ext-real-membered set ; clusterF "" -> non empty ext-real-membered ; coherence not F "" is empty proof the Element of F " in F "" by Th21; hence not F "" is empty ; ::_thesis: verum end; end; theorem :: MEMBER_1:22 for F, G being ext-real-membered set st F c= G holds F "" c= G "" proof let F, G be ext-real-membered set ; ::_thesis: ( F c= G implies F "" c= G "" ) assume A1: F c= G ; ::_thesis: F "" c= G "" let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F "" or i in G "" ) assume i in F "" ; ::_thesis: i in G "" then ex w being Element of ExtREAL st ( i = w " & w in F ) ; hence i in G "" by A1; ::_thesis: verum end; theorem Th23: :: MEMBER_1:23 for F, G being ext-real-membered set holds (F \/ G) "" = (F "") \/ (G "") proof let F, G be ext-real-membered set ; ::_thesis: (F \/ G) "" = (F "") \/ (G "") let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F \/ G) "" or i in (F "") \/ (G "") ) & ( not i in (F "") \/ (G "") or i in (F \/ G) "" ) ) hereby ::_thesis: ( not i in (F "") \/ (G "") or i in (F \/ G) "" ) assume i in (F \/ G) "" ; ::_thesis: i in (F "") \/ (G "") then consider w being Element of ExtREAL such that A1: i = w " and A2: w in F \/ G ; ( w in F or w in G ) by A2, XBOOLE_0:def_3; then ( w " in F "" or w " in G "" ) ; hence i in (F "") \/ (G "") by A1, XBOOLE_0:def_3; ::_thesis: verum end; assume A3: i in (F "") \/ (G "") ; ::_thesis: i in (F \/ G) "" percases ( i in F "" or i in G "" ) by A3, XBOOLE_0:def_3; suppose i in F "" ; ::_thesis: i in (F \/ G) "" then consider w being Element of ExtREAL such that A4: i = w " and A5: w in F ; w in F \/ G by A5, XBOOLE_0:def_3; hence i in (F \/ G) "" by A4; ::_thesis: verum end; suppose i in G "" ; ::_thesis: i in (F \/ G) "" then consider w being Element of ExtREAL such that A6: i = w " and A7: w in G ; w in F \/ G by A7, XBOOLE_0:def_3; hence i in (F \/ G) "" by A6; ::_thesis: verum end; end; end; theorem Th24: :: MEMBER_1:24 for F, G being ext-real-membered set holds (F /\ G) "" c= (F "") /\ (G "") proof let F, G be ext-real-membered set ; ::_thesis: (F /\ G) "" c= (F "") /\ (G "") let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (F /\ G) "" or i in (F "") /\ (G "") ) assume i in (F /\ G) "" ; ::_thesis: i in (F "") /\ (G "") then consider w being Element of ExtREAL such that A1: i = w " and A2: w in F /\ G ; w in G by A2, XBOOLE_0:def_4; then A3: w " in G "" ; w in F by A2, XBOOLE_0:def_4; then w " in F "" ; hence i in (F "") /\ (G "") by A1, A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: MEMBER_1:25 for F being ext-real-membered set holds -- (F "") = (-- F) "" proof let F be ext-real-membered set ; ::_thesis: -- (F "") = (-- F) "" let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F "") or i in (-- F) "" ) & ( not i in (-- F) "" or i in -- (F "") ) ) hereby ::_thesis: ( not i in (-- F) "" or i in -- (F "") ) assume i in -- (F "") ; ::_thesis: i in (-- F) "" then - i in F "" by Th2; then consider w being Element of ExtREAL such that A1: - i = w " and A2: w in F ; ( (- w) " = - (w ") & - w in -- F ) by A2, XXREAL_3:99; hence i in (-- F) "" by A1; ::_thesis: verum end; assume i in (-- F) "" ; ::_thesis: i in -- (F "") then consider w being Element of ExtREAL such that A3: i = w " and A4: w in -- F ; ( (- w) " = - (w ") & - w in F ) by A4, Th2, XXREAL_3:99; then - i in F "" by A3; hence i in -- (F "") by Th2; ::_thesis: verum end; theorem Th26: :: MEMBER_1:26 for f being ext-real number holds {f} "" = {(f ")} proof let f be ext-real number ; ::_thesis: {f} "" = {(f ")} let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in {f} "" or i in {(f ")} ) & ( not i in {(f ")} or i in {f} "" ) ) hereby ::_thesis: ( not i in {(f ")} or i in {f} "" ) assume i in {f} "" ; ::_thesis: i in {(f ")} then consider w being Element of ExtREAL such that A1: i = w " and A2: w in {f} ; w = f by A2, TARSKI:def_1; hence i in {(f ")} by A1, TARSKI:def_1; ::_thesis: verum end; assume i in {(f ")} ; ::_thesis: i in {f} "" then A3: i = f " by TARSKI:def_1; ( f in ExtREAL & f in {f} ) by TARSKI:def_1, XXREAL_0:def_1; hence i in {f} "" by A3; ::_thesis: verum end; theorem Th27: :: MEMBER_1:27 for f, g being ext-real number holds {f,g} "" = {(f "),(g ")} proof let f, g be ext-real number ; ::_thesis: {f,g} "" = {(f "),(g ")} thus {f,g} "" = ({f} \/ {g}) "" by ENUMSET1:1 .= ({f} "") \/ ({g} "") by Th23 .= {(f ")} \/ ({g} "") by Th26 .= {(f ")} \/ {(g ")} by Th26 .= {(f "),(g ")} by ENUMSET1:1 ; ::_thesis: verum end; definition let A be complex-membered set ; funcA "" -> complex-membered set equals :: MEMBER_1:def 4 { (c ") where c is Element of COMPLEX : c in A } ; coherence { (c ") where c is Element of COMPLEX : c in A } is complex-membered set proof { (c ") where c is Element of COMPLEX : c in A } is complex-membered proof let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in { (c ") where c is Element of COMPLEX : c in A } or e is complex ) assume e in { (c ") where c is Element of COMPLEX : c in A } ; ::_thesis: e is complex then ex c being Element of COMPLEX st ( e = c " & c in A ) ; hence e is complex ; ::_thesis: verum end; hence { (c ") where c is Element of COMPLEX : c in A } is complex-membered set ; ::_thesis: verum end; involutiveness for b1, b2 being complex-membered set st b1 = { (c ") where c is Element of COMPLEX : c in b2 } holds b2 = { (c ") where c is Element of COMPLEX : c in b1 } proof let A, B be complex-membered set ; ::_thesis: ( A = { (c ") where c is Element of COMPLEX : c in B } implies B = { (c ") where c is Element of COMPLEX : c in A } ) assume A1: A = { (c ") where c is Element of COMPLEX : c in B } ; ::_thesis: B = { (c ") where c is Element of COMPLEX : c in A } thus B c= { (c ") where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c ") where c is Element of COMPLEX : c in A } c= B proof let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in B or z in { (c ") where c is Element of COMPLEX : c in A } ) A2: z in COMPLEX by XCMPLX_0:def_2; A3: ( z " in COMPLEX & z = (z ") " ) by XCMPLX_0:def_2; assume z in B ; ::_thesis: z in { (c ") where c is Element of COMPLEX : c in A } then z " in A by A1, A2; hence z in { (c ") where c is Element of COMPLEX : c in A } by A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c ") where c is Element of COMPLEX : c in A } or e in B ) assume e in { (c ") where c is Element of COMPLEX : c in A } ; ::_thesis: e in B then consider r0 being Element of COMPLEX such that A4: r0 " = e and A5: r0 in A ; ex c being Element of COMPLEX st ( c " = r0 & c in B ) by A1, A5; hence e in B by A4; ::_thesis: verum end; end; :: deftheorem defines "" MEMBER_1:def_4_:_ for A being complex-membered set holds A "" = { (c ") where c is Element of COMPLEX : c in A } ; theorem Th28: :: MEMBER_1:28 for A being complex-membered set for a being complex number holds ( a in A iff a " in A "" ) proof let A be complex-membered set ; ::_thesis: for a being complex number holds ( a in A iff a " in A "" ) let a be complex number ; ::_thesis: ( a in A iff a " in A "" ) a in COMPLEX by XCMPLX_0:def_2; hence ( a in A implies a " in A "" ) ; ::_thesis: ( a " in A "" implies a in A ) assume a " in A "" ; ::_thesis: a in A then ex c being Element of COMPLEX st ( c " = a " & c in A ) ; hence a in A by XCMPLX_1:201; ::_thesis: verum end; theorem Th29: :: MEMBER_1:29 for A being complex-membered set for a being complex number holds ( a " in A iff a in A "" ) proof let A be complex-membered set ; ::_thesis: for a being complex number holds ( a " in A iff a in A "" ) let a be complex number ; ::_thesis: ( a " in A iff a in A "" ) (a ") " = a ; hence ( a " in A iff a in A "" ) by Th28; ::_thesis: verum end; registration let A be empty set ; clusterA "" -> empty complex-membered ; coherence A "" is empty proof assume not A "" is empty ; ::_thesis: contradiction then the Element of A "" in A "" ; then ex c being Element of COMPLEX st ( the Element of A "" = c " & c in A ) ; hence contradiction ; ::_thesis: verum end; end; registration let A be non empty complex-membered set ; clusterA "" -> non empty complex-membered ; coherence not A "" is empty proof the Element of A " in A "" by Th28; hence not A "" is empty ; ::_thesis: verum end; end; registration let A be real-membered set ; clusterA "" -> complex-membered real-membered ; coherence A "" is real-membered proof let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A "" or e is real ) assume e in A "" ; ::_thesis: e is real then ex c being Element of COMPLEX st ( e = c " & c in A ) ; hence e is real ; ::_thesis: verum end; end; registration let A be rational-membered set ; clusterA "" -> complex-membered rational-membered ; coherence A "" is rational-membered proof let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A "" or e is rational ) assume e in A "" ; ::_thesis: e is rational then ex c being Element of COMPLEX st ( e = c " & c in A ) ; hence e is rational ; ::_thesis: verum end; end; registration let A be real-membered set ; let F be ext-real-membered set ; identifyA "" with F "" when A = F; compatibility ( A = F implies A "" = F "" ) proof assume A1: A = F ; ::_thesis: A "" = F "" let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A "" or a in F "" ) & ( not a in F "" or a in A "" ) ) hereby ::_thesis: ( not a in F "" or a in A "" ) assume a in A "" ; ::_thesis: a in F "" then consider c being Element of COMPLEX such that A2: a = c " and A3: c in A ; reconsider w = c as Element of ExtREAL by A3, XXREAL_0:def_1; ex m being complex number st ( w = m & w " = m " ) by A3, XXREAL_3:def_6; hence a in F "" by A1, A2, A3; ::_thesis: verum end; assume a in F "" ; ::_thesis: a in A "" then consider w being Element of ExtREAL such that A4: a = w " and A5: w in F ; reconsider c = w as Element of COMPLEX by A1, A5, XCMPLX_0:def_2; w " = c " by A1, A5, XXREAL_3:def_6; hence a in A "" by A1, A4, A5; ::_thesis: verum end; end; Lm3: for A, B being complex-membered set st A c= B holds A "" c= B "" proof let A, B be complex-membered set ; ::_thesis: ( A c= B implies A "" c= B "" ) assume A1: A c= B ; ::_thesis: A "" c= B "" let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A "" or a in B "" ) assume a in A "" ; ::_thesis: a in B "" then a " in A by Th29; hence a in B "" by A1, Th29; ::_thesis: verum end; theorem Th30: :: MEMBER_1:30 for A, B being complex-membered set holds ( A c= B iff A "" c= B "" ) proof let A, B be complex-membered set ; ::_thesis: ( A c= B iff A "" c= B "" ) ( (A "") "" = A & (B "") "" = B ) ; hence ( A c= B iff A "" c= B "" ) by Lm3; ::_thesis: verum end; theorem :: MEMBER_1:31 for A, B being complex-membered set st A "" = B "" holds A = B proof let A, B be complex-membered set ; ::_thesis: ( A "" = B "" implies A = B ) assume A "" = B "" ; ::_thesis: A = B then ( A c= B & B c= A ) by Th30; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th32: :: MEMBER_1:32 for A, B being complex-membered set holds (A \/ B) "" = (A "") \/ (B "") proof let A, B be complex-membered set ; ::_thesis: (A \/ B) "" = (A "") \/ (B "") let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A \/ B) "" or a in (A "") \/ (B "") ) & ( not a in (A "") \/ (B "") or a in (A \/ B) "" ) ) hereby ::_thesis: ( not a in (A "") \/ (B "") or a in (A \/ B) "" ) assume a in (A \/ B) "" ; ::_thesis: a in (A "") \/ (B "") then a " in A \/ B by Th29; then ( a " in A or a " in B ) by XBOOLE_0:def_3; then ( a in A "" or a in B "" ) by Th29; hence a in (A "") \/ (B "") by XBOOLE_0:def_3; ::_thesis: verum end; assume a in (A "") \/ (B "") ; ::_thesis: a in (A \/ B) "" then ( a in A "" or a in B "" ) by XBOOLE_0:def_3; then ( a " in A or a " in B ) by Th29; then a " in A \/ B by XBOOLE_0:def_3; hence a in (A \/ B) "" by Th29; ::_thesis: verum end; theorem Th33: :: MEMBER_1:33 for A, B being complex-membered set holds (A /\ B) "" = (A "") /\ (B "") proof let A, B be complex-membered set ; ::_thesis: (A /\ B) "" = (A "") /\ (B "") let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A /\ B) "" or a in (A "") /\ (B "") ) & ( not a in (A "") /\ (B "") or a in (A /\ B) "" ) ) hereby ::_thesis: ( not a in (A "") /\ (B "") or a in (A /\ B) "" ) assume a in (A /\ B) "" ; ::_thesis: a in (A "") /\ (B "") then A1: a " in A /\ B by Th29; then a " in B by XBOOLE_0:def_4; then A2: a in B "" by Th29; a " in A by A1, XBOOLE_0:def_4; then a in A "" by Th29; hence a in (A "") /\ (B "") by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: a in (A "") /\ (B "") ; ::_thesis: a in (A /\ B) "" then a in B "" by XBOOLE_0:def_4; then A4: a " in B by Th29; a in A "" by A3, XBOOLE_0:def_4; then a " in A by Th29; then a " in A /\ B by A4, XBOOLE_0:def_4; hence a in (A /\ B) "" by Th29; ::_thesis: verum end; theorem Th34: :: MEMBER_1:34 for A, B being complex-membered set holds (A \ B) "" = (A "") \ (B "") proof let A, B be complex-membered set ; ::_thesis: (A \ B) "" = (A "") \ (B "") let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A \ B) "" or a in (A "") \ (B "") ) & ( not a in (A "") \ (B "") or a in (A \ B) "" ) ) hereby ::_thesis: ( not a in (A "") \ (B "") or a in (A \ B) "" ) assume a in (A \ B) "" ; ::_thesis: a in (A "") \ (B "") then A1: a " in A \ B by Th29; then not a " in B by XBOOLE_0:def_5; then A2: not a in B "" by Th29; a in A "" by A1, Th29; hence a in (A "") \ (B "") by A2, XBOOLE_0:def_5; ::_thesis: verum end; assume A3: a in (A "") \ (B "") ; ::_thesis: a in (A \ B) "" then not a in B "" by XBOOLE_0:def_5; then A4: not a " in B by Th29; a " in A by A3, Th29; then a " in A \ B by A4, XBOOLE_0:def_5; hence a in (A \ B) "" by Th29; ::_thesis: verum end; theorem Th35: :: MEMBER_1:35 for A, B being complex-membered set holds (A \+\ B) "" = (A "") \+\ (B "") proof let A, B be complex-membered set ; ::_thesis: (A \+\ B) "" = (A "") \+\ (B "") thus (A \+\ B) "" = ((A \ B) "") \/ ((B \ A) "") by Th32 .= ((A "") \ (B "")) \/ ((B \ A) "") by Th34 .= (A "") \+\ (B "") by Th34 ; ::_thesis: verum end; theorem Th36: :: MEMBER_1:36 for A being complex-membered set holds -- (A "") = (-- A) "" proof let A be complex-membered set ; ::_thesis: -- (A "") = (-- A) "" let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in -- (A "") or a in (-- A) "" ) & ( not a in (-- A) "" or a in -- (A "") ) ) A1: (- a) " = - (a ") by XCMPLX_1:222; hereby ::_thesis: ( not a in (-- A) "" or a in -- (A "") ) assume a in -- (A "") ; ::_thesis: a in (-- A) "" then - a in A "" by Th12; then (- a) " in A by Th29; then a " in -- A by A1, Th12; hence a in (-- A) "" by Th29; ::_thesis: verum end; assume a in (-- A) "" ; ::_thesis: a in -- (A "") then a " in -- A by Th29; then - (a ") in A by Th12; then - a in A "" by A1, Th29; hence a in -- (A "") by Th12; ::_thesis: verum end; theorem Th37: :: MEMBER_1:37 for a being complex number holds {a} "" = {(a ")} proof let a be complex number ; ::_thesis: {a} "" = {(a ")} let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} "" or z in {(a ")} ) & ( not z in {(a ")} or z in {a} "" ) ) hereby ::_thesis: ( not z in {(a ")} or z in {a} "" ) assume z in {a} "" ; ::_thesis: z in {(a ")} then consider c being Element of COMPLEX such that A1: z = c " and A2: c in {a} ; c = a by A2, TARSKI:def_1; hence z in {(a ")} by A1, TARSKI:def_1; ::_thesis: verum end; assume z in {(a ")} ; ::_thesis: z in {a} "" then A3: z = a " by TARSKI:def_1; ( a in COMPLEX & a in {a} ) by TARSKI:def_1, XCMPLX_0:def_2; hence z in {a} "" by A3; ::_thesis: verum end; theorem Th38: :: MEMBER_1:38 for a, b being complex number holds {a,b} "" = {(a "),(b ")} proof let a, b be complex number ; ::_thesis: {a,b} "" = {(a "),(b ")} let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a,b} "" or z in {(a "),(b ")} ) & ( not z in {(a "),(b ")} or z in {a,b} "" ) ) hereby ::_thesis: ( not z in {(a "),(b ")} or z in {a,b} "" ) assume z in {a,b} "" ; ::_thesis: z in {(a "),(b ")} then consider c being Element of COMPLEX such that A1: z = c " and A2: c in {a,b} ; ( c = a or c = b ) by A2, TARSKI:def_2; hence z in {(a "),(b ")} by A1, TARSKI:def_2; ::_thesis: verum end; A3: ( a in {a,b} & b in {a,b} ) by TARSKI:def_2; assume z in {(a "),(b ")} ; ::_thesis: z in {a,b} "" then A4: ( z = a " or z = b " ) by TARSKI:def_2; ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; hence z in {a,b} "" by A4, A3; ::_thesis: verum end; definition let F, G be ext-real-membered set ; funcF ++ G -> set equals :: MEMBER_1:def 5 { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; coherence { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ; commutativity for b1 being set for F, G being ext-real-membered set st b1 = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds b1 = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } proof let X be set ; ::_thesis: for F, G being ext-real-membered set st X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } let F, G be ext-real-membered set ; ::_thesis: ( X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } implies X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ) assume A1: X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } thus X c= { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ) assume e in X ; ::_thesis: e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } then ex w1, w2 being Element of ExtREAL st ( e = w1 + w2 & w1 in F & w2 in G ) by A1; hence e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } or e in X ) assume e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: e in X then ex w1, w2 being Element of ExtREAL st ( e = w1 + w2 & w1 in G & w2 in F ) ; hence e in X by A1; ::_thesis: verum end; end; :: deftheorem defines ++ MEMBER_1:def_5_:_ for F, G being ext-real-membered set holds F ++ G = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; theorem Th39: :: MEMBER_1:39 for F, G being ext-real-membered set for f, g being ext-real number st f in F & g in G holds f + g in F ++ G proof let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds f + g in F ++ G let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f + g in F ++ G ) ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; hence ( f in F & g in G implies f + g in F ++ G ) ; ::_thesis: verum end; registration let F be empty set ; let G be ext-real-membered set ; clusterF ++ G -> empty ; coherence F ++ G is empty proof assume not F ++ G is empty ; ::_thesis: contradiction then the Element of F ++ G in F ++ G ; then ex w1, w2 being Element of ExtREAL st ( the Element of F ++ G = w1 + w2 & w1 in F & w2 in G ) ; hence contradiction ; ::_thesis: verum end; clusterG ++ F -> empty ; coherence G ++ F is empty ; end; registration let F, G be non empty ext-real-membered set ; clusterF ++ G -> non empty ; coherence not F ++ G is empty proof the Element of F + the Element of G in F ++ G by Th39; hence not F ++ G is empty ; ::_thesis: verum end; end; registration let F, G be ext-real-membered set ; clusterF ++ G -> ext-real-membered ; coherence F ++ G is ext-real-membered proof let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in F ++ G or e is ext-real ) assume e in F ++ G ; ::_thesis: e is ext-real then ex w1, w2 being Element of ExtREAL st ( e = w1 + w2 & w1 in F & w2 in G ) ; hence e is ext-real ; ::_thesis: verum 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 let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F ++ H c= G ++ I ) assume A1: ( F c= G & H c= I ) ; ::_thesis: F ++ H c= G ++ I let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F ++ H or i in G ++ I ) assume i in F ++ H ; ::_thesis: i in G ++ I then ex w, w1 being Element of ExtREAL st ( i = w + w1 & w in F & w1 in H ) ; hence i in G ++ I by A1; ::_thesis: verum end; theorem Th41: :: MEMBER_1:41 for F, G, H being ext-real-membered set holds F ++ (G \/ H) = (F ++ G) \/ (F ++ H) proof let F, G, H be ext-real-membered set ; ::_thesis: F ++ (G \/ H) = (F ++ G) \/ (F ++ H) let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in F ++ (G \/ H) or j in (F ++ G) \/ (F ++ H) ) & ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) ) ) hereby ::_thesis: ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) ) assume j in F ++ (G \/ H) ; ::_thesis: j in (F ++ G) \/ (F ++ H) then consider w, w1 being Element of ExtREAL such that A1: j = w + w1 and A2: w in F and A3: w1 in G \/ H ; ( w1 in G or w1 in H ) by A3, XBOOLE_0:def_3; then ( w + w1 in F ++ G or w + w1 in F ++ H ) by A2; hence j in (F ++ G) \/ (F ++ H) by A1, XBOOLE_0:def_3; ::_thesis: verum end; assume A4: j in (F ++ G) \/ (F ++ H) ; ::_thesis: j in F ++ (G \/ H) percases ( j in F ++ G or j in F ++ H ) by A4, XBOOLE_0:def_3; suppose j in F ++ G ; ::_thesis: j in F ++ (G \/ H) then consider w, w1 being Element of ExtREAL such that A5: ( j = w + w1 & w in F ) and A6: w1 in G ; w1 in G \/ H by A6, XBOOLE_0:def_3; hence j in F ++ (G \/ H) by A5; ::_thesis: verum end; suppose j in F ++ H ; ::_thesis: j in F ++ (G \/ H) then consider w, w1 being Element of ExtREAL such that A7: ( j = w + w1 & w in F ) and A8: w1 in H ; w1 in G \/ H by A8, XBOOLE_0:def_3; hence j in F ++ (G \/ H) by A7; ::_thesis: verum end; end; 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 let F, G, H be ext-real-membered set ; ::_thesis: F ++ (G /\ H) c= (F ++ G) /\ (F ++ H) let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in F ++ (G /\ H) or j in (F ++ G) /\ (F ++ H) ) assume j in F ++ (G /\ H) ; ::_thesis: j in (F ++ G) /\ (F ++ H) then consider w, w1 being Element of ExtREAL such that A1: j = w + w1 and A2: w in F and A3: w1 in G /\ H ; w1 in H by A3, XBOOLE_0:def_4; then A4: w + w1 in F ++ H by A2; w1 in G by A3, XBOOLE_0:def_4; then w + w1 in F ++ G by A2; hence j in (F ++ G) /\ (F ++ H) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th43: :: MEMBER_1:43 for f, g being ext-real number holds {f} ++ {g} = {(f + g)} proof let f, g be ext-real number ; ::_thesis: {f} ++ {g} = {(f + g)} let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in {f} ++ {g} or j in {(f + g)} ) & ( not j in {(f + g)} or j in {f} ++ {g} ) ) hereby ::_thesis: ( not j in {(f + g)} or j in {f} ++ {g} ) assume j in {f} ++ {g} ; ::_thesis: j in {(f + g)} then consider w1, w2 being Element of ExtREAL such that A1: j = w1 + w2 and A2: ( w1 in {f} & w2 in {g} ) ; ( w1 = f & w2 = g ) by A2, TARSKI:def_1; hence j in {(f + g)} by A1, TARSKI:def_1; ::_thesis: verum end; A3: ( f in {f} & g in {g} ) by TARSKI:def_1; assume j in {(f + g)} ; ::_thesis: j in {f} ++ {g} then A4: j = f + g by TARSKI:def_1; ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; hence j in {f} ++ {g} by A4, A3; ::_thesis: verum end; theorem Th44: :: MEMBER_1:44 for f, g, h being ext-real number holds {f} ++ {g,h} = {(f + g),(f + h)} proof let f, g, h be ext-real number ; ::_thesis: {f} ++ {g,h} = {(f + g),(f + h)} thus {f} ++ {g,h} = {f} ++ ({g} \/ {h}) by ENUMSET1:1 .= ({f} ++ {g}) \/ ({f} ++ {h}) by Th41 .= {(f + g)} \/ ({f} ++ {h}) by Th43 .= {(f + g)} \/ {(f + h)} by Th43 .= {(f + g),(f + h)} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th45: :: MEMBER_1:45 for f, g, h, i being ext-real number holds {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)} proof let f, g, h, i be ext-real number ; ::_thesis: {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)} thus {f,g} ++ {h,i} = ({f} \/ {g}) ++ {h,i} by ENUMSET1:1 .= ({f} ++ {h,i}) \/ ({g} ++ {h,i}) by Th41 .= {(f + h),(f + i)} \/ ({g} ++ {h,i}) by Th44 .= {(f + h),(f + i)} \/ {(g + h),(g + i)} by Th44 .= {(f + h),(f + i),(g + h),(g + i)} by ENUMSET1:5 ; ::_thesis: verum end; definition let A, B be complex-membered set ; funcA ++ B -> set equals :: MEMBER_1:def 6 { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; coherence { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ; commutativity for b1 being set for A, B being complex-membered set st b1 = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds b1 = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } proof let X be set ; ::_thesis: for A, B being complex-membered set st X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } let A, B be complex-membered set ; ::_thesis: ( X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } implies X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ) assume A1: X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } thus X c= { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ) assume e in X ; ::_thesis: e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) by A1; hence e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } or e in X ) assume e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: e in X then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in B & c2 in A ) ; hence e in X by A1; ::_thesis: verum end; end; :: deftheorem defines ++ MEMBER_1:def_6_:_ for A, B being complex-membered set holds A ++ B = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; theorem Th46: :: MEMBER_1:46 for A, B being complex-membered set for a, b being complex number st a in A & b in B holds a + b in A ++ B proof let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds a + b in A ++ B let a, b be complex number ; ::_thesis: ( a in A & b in B implies a + b in A ++ B ) ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; hence ( a in A & b in B implies a + b in A ++ B ) ; ::_thesis: verum end; registration let A be empty set ; let B be complex-membered set ; clusterA ++ B -> empty ; coherence A ++ B is empty proof assume not A ++ B is empty ; ::_thesis: contradiction then the Element of A ++ B in A ++ B ; then ex c1, c2 being Element of COMPLEX st ( the Element of A ++ B = c1 + c2 & c1 in A & c2 in B ) ; hence contradiction ; ::_thesis: verum end; clusterB ++ A -> empty ; coherence B ++ A is empty ; end; registration let A, B be non empty complex-membered set ; clusterA ++ B -> non empty ; coherence not A ++ B is empty proof the Element of A + the Element of B in A ++ B by Th46; hence not A ++ B is empty ; ::_thesis: verum end; end; registration let A, B be complex-membered set ; clusterA ++ B -> complex-membered ; coherence A ++ B is complex-membered proof let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in A ++ B or e is complex ) assume e in A ++ B ; ::_thesis: e is complex then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) ; hence e is complex ; ::_thesis: verum end; end; registration let A, B be real-membered set ; clusterA ++ B -> real-membered ; coherence A ++ B is real-membered proof let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A ++ B or e is real ) assume e in A ++ B ; ::_thesis: e is real then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) ; hence e is real ; ::_thesis: verum end; end; registration let A, B be rational-membered set ; clusterA ++ B -> rational-membered ; coherence A ++ B is rational-membered proof let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A ++ B or e is rational ) assume e in A ++ B ; ::_thesis: e is rational then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) ; hence e is rational ; ::_thesis: verum end; end; registration let A, B be integer-membered set ; clusterA ++ B -> integer-membered ; coherence A ++ B is integer-membered proof let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in A ++ B or e is integer ) assume e in A ++ B ; ::_thesis: e is integer then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) ; hence e is integer ; ::_thesis: verum end; end; registration let A, B be natural-membered set ; clusterA ++ B -> natural-membered ; coherence A ++ B is natural-membered proof let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( not e in A ++ B or e is natural ) assume e in A ++ B ; ::_thesis: e is natural then ex c1, c2 being Element of COMPLEX st ( e = c1 + c2 & c1 in A & c2 in B ) ; hence e is natural ; ::_thesis: verum end; end; registration let A, B be real-membered set ; let F, G be ext-real-membered set ; identifyA ++ B with F ++ G when A = F, B = G; compatibility ( A = F & B = G implies A ++ B = F ++ G ) proof assume A1: ( A = F & B = G ) ; ::_thesis: A ++ B = F ++ G let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A ++ B or a in F ++ G ) & ( not a in F ++ G or a in A ++ B ) ) hereby ::_thesis: ( not a in F ++ G or a in A ++ B ) assume a in A ++ B ; ::_thesis: a in F ++ G then consider c, c1 being Element of COMPLEX such that A2: a = c + c1 and A3: ( c in A & c1 in B ) ; reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def_1; a = d1 + d2 by A2, A3, XXREAL_3:def_2; hence a in F ++ G by A1, A3; ::_thesis: verum end; assume a in F ++ G ; ::_thesis: a in A ++ B then consider w, w1 being Element of ExtREAL such that A4: a = w + w1 and A5: ( w in F & w1 in G ) ; reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def_2; a = d1 + d2 by A1, A4, A5, XXREAL_3:def_2; hence a in A ++ B by A1, A5; ::_thesis: verum 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 let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A ++ C c= B ++ D ) assume A1: ( A c= B & C c= D ) ; ::_thesis: A ++ C c= B ++ D let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ++ C or a in B ++ D ) assume a in A ++ C ; ::_thesis: a in B ++ D then ex c, c1 being Element of COMPLEX st ( a = c + c1 & c in A & c1 in C ) ; hence a in B ++ D by A1; ::_thesis: verum end; theorem Th48: :: MEMBER_1:48 for A, B, C being complex-membered set holds A ++ (B \/ C) = (A ++ B) \/ (A ++ C) proof let A, B, C be complex-membered set ; ::_thesis: A ++ (B \/ C) = (A ++ B) \/ (A ++ C) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ++ (B \/ C) or a in (A ++ B) \/ (A ++ C) ) & ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) ) ) hereby ::_thesis: ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) ) assume a in A ++ (B \/ C) ; ::_thesis: a in (A ++ B) \/ (A ++ C) then consider c, c1 being Element of COMPLEX such that A1: a = c + c1 and A2: c in A and A3: c1 in B \/ C ; ( c1 in B or c1 in C ) by A3, XBOOLE_0:def_3; then ( c + c1 in A ++ B or c + c1 in A ++ C ) by A2; hence a in (A ++ B) \/ (A ++ C) by A1, XBOOLE_0:def_3; ::_thesis: verum end; assume A4: a in (A ++ B) \/ (A ++ C) ; ::_thesis: a in A ++ (B \/ C) percases ( a in A ++ B or a in A ++ C ) by A4, XBOOLE_0:def_3; suppose a in A ++ B ; ::_thesis: a in A ++ (B \/ C) then consider c, c1 being Element of COMPLEX such that A5: ( a = c + c1 & c in A ) and A6: c1 in B ; c1 in B \/ C by A6, XBOOLE_0:def_3; hence a in A ++ (B \/ C) by A5; ::_thesis: verum end; suppose a in A ++ C ; ::_thesis: a in A ++ (B \/ C) then consider c, c1 being Element of COMPLEX such that A7: ( a = c + c1 & c in A ) and A8: c1 in C ; c1 in B \/ C by A8, XBOOLE_0:def_3; hence a in A ++ (B \/ C) by A7; ::_thesis: verum end; end; end; theorem Th49: :: MEMBER_1:49 for A, B, C being complex-membered set holds A ++ (B /\ C) c= (A ++ B) /\ (A ++ C) proof let A, B, C be complex-membered set ; ::_thesis: A ++ (B /\ C) c= (A ++ B) /\ (A ++ C) let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ++ (B /\ C) or a in (A ++ B) /\ (A ++ C) ) assume a in A ++ (B /\ C) ; ::_thesis: a in (A ++ B) /\ (A ++ C) then consider c, c1 being Element of COMPLEX such that A1: a = c + c1 and A2: c in A and A3: c1 in B /\ C ; c1 in C by A3, XBOOLE_0:def_4; then A4: c + c1 in A ++ C by A2; c1 in B by A3, XBOOLE_0:def_4; then c + c1 in A ++ B by A2; hence a in (A ++ B) /\ (A ++ C) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th50: :: MEMBER_1:50 for A, B, C being complex-membered set holds (A ++ B) ++ C = A ++ (B ++ C) proof let A, B, C be complex-membered set ; ::_thesis: (A ++ B) ++ C = A ++ (B ++ C) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ++ B) ++ C or a in A ++ (B ++ C) ) & ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C ) ) hereby ::_thesis: ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C ) assume a in (A ++ B) ++ C ; ::_thesis: a in A ++ (B ++ C) then consider c, c1 being Element of COMPLEX such that A1: a = c + c1 and A2: c in A ++ B and A3: c1 in C ; consider c2, c3 being Element of COMPLEX such that A4: c = c2 + c3 and A5: c2 in A and A6: c3 in B by A2; ( a = c2 + (c3 + c1) & c3 + c1 in B ++ C ) by A1, A3, A4, A6; hence a in A ++ (B ++ C) by A5; ::_thesis: verum end; assume a in A ++ (B ++ C) ; ::_thesis: a in (A ++ B) ++ C then consider c, c1 being Element of COMPLEX such that A7: ( a = c + c1 & c in A ) and A8: c1 in B ++ C ; consider c2, c3 being Element of COMPLEX such that A9: ( c1 = c2 + c3 & c2 in B ) and A10: c3 in C by A8; ( a = (c + c2) + c3 & c + c2 in A ++ B ) by A7, A9; hence a in (A ++ B) ++ C by A10; ::_thesis: verum end; theorem Th51: :: MEMBER_1:51 for a, b being complex number holds {a} ++ {b} = {(a + b)} proof let a, b be complex number ; ::_thesis: {a} ++ {b} = {(a + b)} let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} ++ {b} or z in {(a + b)} ) & ( not z in {(a + b)} or z in {a} ++ {b} ) ) hereby ::_thesis: ( not z in {(a + b)} or z in {a} ++ {b} ) assume z in {a} ++ {b} ; ::_thesis: z in {(a + b)} then consider c1, c2 being Element of COMPLEX such that A1: z = c1 + c2 and A2: ( c1 in {a} & c2 in {b} ) ; ( c1 = a & c2 = b ) by A2, TARSKI:def_1; hence z in {(a + b)} by A1, TARSKI:def_1; ::_thesis: verum end; A3: ( a in {a} & b in {b} ) by TARSKI:def_1; assume z in {(a + b)} ; ::_thesis: z in {a} ++ {b} then A4: z = a + b by TARSKI:def_1; ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; hence z in {a} ++ {b} by A4, A3; ::_thesis: verum end; theorem Th52: :: MEMBER_1:52 for a, s, t being complex number holds {a} ++ {s,t} = {(a + s),(a + t)} proof let a, s, t be complex number ; ::_thesis: {a} ++ {s,t} = {(a + s),(a + t)} thus {a} ++ {s,t} = {a} ++ ({s} \/ {t}) by ENUMSET1:1 .= ({a} ++ {s}) \/ ({a} ++ {t}) by Th48 .= {(a + s)} \/ ({a} ++ {t}) by Th51 .= {(a + s)} \/ {(a + t)} by Th51 .= {(a + s),(a + t)} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th53: :: MEMBER_1:53 for a, b, s, t being complex number holds {a,b} ++ {s,t} = {(a + s),(a + t),(b + s),(b + t)} proof let a, b, s, t be complex number ; ::_thesis: {a,b} ++ {s,t} = {(a + s),(a + t),(b + s),(b + t)} thus {a,b} ++ {s,t} = ({a} \/ {b}) ++ {s,t} by ENUMSET1:1 .= ({a} ++ {s,t}) \/ ({b} ++ {s,t}) by Th48 .= {(a + s),(a + t)} \/ ({b} ++ {s,t}) by Th52 .= {(a + s),(a + t)} \/ {(b + s),(b + t)} by Th52 .= {(a + s),(a + t),(b + s),(b + t)} by ENUMSET1:5 ; ::_thesis: verum end; definition let F, G be ext-real-membered set ; funcF -- G -> set equals :: MEMBER_1:def 7 F ++ (-- G); coherence F ++ (-- G) is set ; end; :: deftheorem defines -- MEMBER_1:def_7_:_ for F, G being ext-real-membered set holds F -- G = F ++ (-- G); theorem Th54: :: MEMBER_1:54 for F, G being ext-real-membered set holds F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } proof let F, G be ext-real-membered set ; ::_thesis: F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } thus F -- G c= { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F -- G proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F -- G or e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ) assume e in F -- G ; ::_thesis: e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 + w2 and A2: w1 in F and A3: w2 in -- G ; ( e = w1 - (- w2) & - w2 in G ) by A1, A3, Th2; hence e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } or e in F -- G ) assume e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: e in F -- G then consider w1, w2 being Element of ExtREAL such that A4: ( e = w1 - w2 & w1 in F ) and A5: w2 in G ; - w2 in -- G by A5; hence e in F -- G by A4; ::_thesis: verum end; theorem Th55: :: MEMBER_1:55 for F, G being ext-real-membered set for f, g being ext-real number st f in F & g in G holds f - g in F -- G proof let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds f - g in F -- G let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f - g in F -- G ) A1: ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by Th54; hence ( f in F & g in G implies f - g in F -- G ) by A1; ::_thesis: verum end; registration let F be empty set ; let G be ext-real-membered set ; clusterF -- G -> empty ; coherence F -- G is empty ; clusterG -- F -> empty ; coherence G -- F is empty ; end; registration let F, G be non empty ext-real-membered set ; clusterF -- G -> non empty ; coherence not F -- G is empty ; end; registration let F, G be ext-real-membered set ; clusterF -- G -> ext-real-membered ; coherence F -- G is ext-real-membered ; end; theorem :: MEMBER_1:56 for F, G, H, I being ext-real-membered set st F c= G & H c= I holds F -- H c= G -- I proof let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F -- H c= G -- I ) assume A1: ( F c= G & H c= I ) ; ::_thesis: F -- H c= G -- I let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F -- H or i in G -- I ) A2: F -- H = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th54; assume i in F -- H ; ::_thesis: i in G -- I then ex w, w1 being Element of ExtREAL st ( i = w - w1 & w in F & w1 in H ) by A2; hence i in G -- I by A1, Th55; ::_thesis: verum end; theorem :: MEMBER_1:57 for F, G, H being ext-real-membered set holds F -- (G \/ H) = (F -- G) \/ (F -- H) proof let F, G, H be ext-real-membered set ; ::_thesis: F -- (G \/ H) = (F -- G) \/ (F -- H) thus F -- (G \/ H) = F ++ ((-- G) \/ (-- H)) by Th5 .= (F -- G) \/ (F -- H) by Th41 ; ::_thesis: verum end; theorem :: MEMBER_1:58 for F, G, H being ext-real-membered set holds F -- (G /\ H) c= (F -- G) /\ (F -- H) proof let F, G, H be ext-real-membered set ; ::_thesis: F -- (G /\ H) c= (F -- G) /\ (F -- H) F -- (G /\ H) = F ++ ((-- G) /\ (-- H)) by Th6; hence F -- (G /\ H) c= (F -- G) /\ (F -- H) by Th42; ::_thesis: verum end; Lm4: for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G) proof let F, G be ext-real-membered set ; ::_thesis: -- (F ++ G) = (-- F) ++ (-- G) let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in -- (F ++ G) or j in (-- F) ++ (-- G) ) & ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) ) ) hereby ::_thesis: ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) ) assume j in -- (F ++ G) ; ::_thesis: j in (-- F) ++ (-- G) then consider w being Element of ExtREAL such that A1: j = - w and A2: w in F ++ G ; consider w1, w2 being Element of ExtREAL such that A3: w = w1 + w2 and A4: ( w1 in F & w2 in G ) by A2; A5: - (w1 + w2) = (- w1) - w2 by XXREAL_3:9; ( - w1 in -- F & - w2 in -- G ) by A4; hence j in (-- F) ++ (-- G) by A1, A3, A5; ::_thesis: verum end; assume j in (-- F) ++ (-- G) ; ::_thesis: j in -- (F ++ G) then consider w1, w2 being Element of ExtREAL such that A6: j = w1 + w2 and A7: ( w1 in -- F & w2 in -- G ) ; ( - w1 in F & - w2 in G ) by A7, Th2; then ( - (w1 + w2) = (- w1) - w2 & (- w1) + (- w2) in F ++ G ) by XXREAL_3:9; hence j in -- (F ++ G) by A6, Th2; ::_thesis: verum 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 let F, G be ext-real-membered set ; ::_thesis: -- (F -- G) = (-- F) ++ G thus -- (F -- G) = (-- F) -- (-- G) by Lm4 .= (-- F) ++ G ; ::_thesis: verum end; theorem :: MEMBER_1:61 for f, g being ext-real number holds {f} -- {g} = {(f - g)} proof let f, g be ext-real number ; ::_thesis: {f} -- {g} = {(f - g)} thus {f} -- {g} = {f} ++ {(- g)} by Th9 .= {(f - g)} by Th43 ; ::_thesis: verum end; theorem :: MEMBER_1:62 for f, h, i being ext-real number holds {f} -- {h,i} = {(f - h),(f - i)} proof let f, h, i be ext-real number ; ::_thesis: {f} -- {h,i} = {(f - h),(f - i)} thus {f} -- {h,i} = {f} ++ {(- h),(- i)} by Th10 .= {(f - h),(f - i)} by Th44 ; ::_thesis: verum end; theorem :: MEMBER_1:63 for f, g, h being ext-real number holds {f,g} -- {h} = {(f - h),(g - h)} proof let f, g, h be ext-real number ; ::_thesis: {f,g} -- {h} = {(f - h),(g - h)} thus {f,g} -- {h} = {f,g} ++ {(- h)} by Th9 .= {(f - h),(g - h)} by Th44 ; ::_thesis: verum end; theorem :: MEMBER_1:64 for f, g, h, i being ext-real number holds {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)} proof let f, g, h, i be ext-real number ; ::_thesis: {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)} thus {f,g} -- {h,i} = {f,g} ++ {(- h),(- i)} by Th10 .= {(f - h),(f - i),(g - h),(g - i)} by Th45 ; ::_thesis: verum end; definition let A, B be complex-membered set ; funcA -- B -> set equals :: MEMBER_1:def 8 A ++ (-- B); coherence A ++ (-- B) is set ; end; :: deftheorem defines -- MEMBER_1:def_8_:_ for A, B being complex-membered set holds A -- B = A ++ (-- B); theorem Th65: :: MEMBER_1:65 for A, B being complex-membered set holds A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } proof let A, B be complex-membered set ; ::_thesis: A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } thus A -- B c= { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } c= A -- B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A -- B or e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ) assume e in A -- B ; ::_thesis: e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } then consider c1, c2 being Element of COMPLEX such that A1: e = c1 + c2 and A2: c1 in A and A3: c2 in -- B ; ( e = c1 - (- c2) & - c2 in B ) by A1, A3, Th12; hence e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by A2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } or e in A -- B ) assume e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: e in A -- B then consider c1, c2 being Element of COMPLEX such that A4: ( e = c1 - c2 & c1 in A ) and A5: c2 in B ; - c2 in -- B by A5; hence e in A -- B by A4; ::_thesis: verum end; theorem Th66: :: MEMBER_1:66 for A, B being complex-membered set for a, b being complex number st a in A & b in B holds a - b in A -- B proof let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds a - b in A -- B let a, b be complex number ; ::_thesis: ( a in A & b in B implies a - b in A -- B ) A1: ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by Th65; hence ( a in A & b in B implies a - b in A -- B ) by A1; ::_thesis: verum end; registration let A be empty set ; let B be complex-membered set ; clusterA -- B -> empty ; coherence A -- B is empty ; clusterB -- A -> empty ; coherence B -- A is empty ; end; registration let A, B be non empty complex-membered set ; clusterA -- B -> non empty ; coherence not A -- B is empty ; end; registration let A, B be complex-membered set ; clusterA -- B -> complex-membered ; coherence A -- B is complex-membered ; end; registration let A, B be real-membered set ; clusterA -- B -> real-membered ; coherence A -- B is real-membered ; end; registration let A, B be rational-membered set ; clusterA -- B -> rational-membered ; coherence A -- B is rational-membered ; end; registration let A, B be integer-membered set ; clusterA -- B -> integer-membered ; coherence A -- B is integer-membered ; end; registration let A, B be real-membered set ; let F, G be ext-real-membered set ; identifyA -- B with F -- G when A = F, B = G; compatibility ( A = F & B = G implies A -- B = F -- G ) ; end; theorem Th67: :: MEMBER_1:67 for A, B, C, D being complex-membered set st A c= B & C c= D holds A -- C c= B -- D proof let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A -- C c= B -- D ) assume A1: ( A c= B & C c= D ) ; ::_thesis: A -- C c= B -- D let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A -- C or z in B -- D ) A2: A -- C = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in C ) } by Th65; assume z in A -- C ; ::_thesis: z in B -- D then ex c, c1 being Element of COMPLEX st ( z = c - c1 & c in A & c1 in C ) by A2; hence z in B -- D by A1, Th66; ::_thesis: verum end; Lm5: for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B) proof let A, B be complex-membered set ; ::_thesis: -- (A ++ B) = (-- A) ++ (-- B) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in -- (A ++ B) or a in (-- A) ++ (-- B) ) & ( not a in (-- A) ++ (-- B) or a in -- (A ++ B) ) ) hereby ::_thesis: ( not a in (-- A) ++ (-- B) or a in -- (A ++ B) ) assume a in -- (A ++ B) ; ::_thesis: a in (-- A) ++ (-- B) then consider c being Element of COMPLEX such that A1: a = - c and A2: c in A ++ B ; consider c1, c2 being Element of COMPLEX such that A3: c = c1 + c2 and A4: ( c1 in A & c2 in B ) by A2; A5: ( - c1 in -- A & - c2 in -- B ) by A4; a = (- c1) + (- c2) by A1, A3; hence a in (-- A) ++ (-- B) by A5; ::_thesis: verum end; assume a in (-- A) ++ (-- B) ; ::_thesis: a in -- (A ++ B) then consider c1, c2 being Element of COMPLEX such that A6: a = c1 + c2 and A7: ( c1 in -- A & c2 in -- B ) ; ( - c1 in A & - c2 in B ) by A7, Th12; then (- c1) + (- c2) in A ++ B ; then - a in A ++ B by A6; hence a in -- (A ++ B) by Th12; ::_thesis: verum end; theorem :: MEMBER_1:68 for A, B, C being complex-membered set holds A -- (B \/ C) = (A -- B) \/ (A -- C) proof let A, B, C be complex-membered set ; ::_thesis: A -- (B \/ C) = (A -- B) \/ (A -- C) thus A -- (B \/ C) = A ++ ((-- B) \/ (-- C)) by Th15 .= (A -- B) \/ (A -- C) by Th48 ; ::_thesis: verum end; theorem :: MEMBER_1:69 for A, B, C being complex-membered set holds A -- (B /\ C) c= (A -- B) /\ (A -- C) proof let A, B, C be complex-membered set ; ::_thesis: A -- (B /\ C) c= (A -- B) /\ (A -- C) A -- (B /\ C) = A ++ ((-- B) /\ (-- C)) by Th16; hence A -- (B /\ C) c= (A -- B) /\ (A -- C) by Th49; ::_thesis: verum 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 let A, B be complex-membered set ; ::_thesis: -- (A -- B) = (-- A) ++ B thus -- (A -- B) = (-- A) -- (-- B) by Lm5 .= (-- A) ++ B ; ::_thesis: verum 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 let A, B, C be complex-membered set ; ::_thesis: A -- (B ++ C) = (A -- B) -- C thus A -- (B ++ C) = A ++ ((-- B) -- C) by Lm5 .= (A -- B) -- C by Th50 ; ::_thesis: verum end; theorem :: MEMBER_1:74 for A, B, C being complex-membered set holds A -- (B -- C) = (A -- B) ++ C proof let A, B, C be complex-membered set ; ::_thesis: A -- (B -- C) = (A -- B) ++ C thus A -- (B -- C) = A ++ ((-- B) ++ C) by Th71 .= (A -- B) ++ C by Th50 ; ::_thesis: verum end; theorem Th75: :: MEMBER_1:75 for a, b being complex number holds {a} -- {b} = {(a - b)} proof let a, b be complex number ; ::_thesis: {a} -- {b} = {(a - b)} thus {a} -- {b} = {a} ++ {(- b)} by Th19 .= {(a - b)} by Th51 ; ::_thesis: verum end; theorem :: MEMBER_1:76 for a, s, t being complex number holds {a} -- {s,t} = {(a - s),(a - t)} proof let a, s, t be complex number ; ::_thesis: {a} -- {s,t} = {(a - s),(a - t)} thus {a} -- {s,t} = {a} ++ {(- s),(- t)} by Th20 .= {(a - s),(a - t)} by Th52 ; ::_thesis: verum end; theorem :: MEMBER_1:77 for a, b, s being complex number holds {a,b} -- {s} = {(a - s),(b - s)} proof let a, b, s be complex number ; ::_thesis: {a,b} -- {s} = {(a - s),(b - s)} thus {a,b} -- {s} = {a,b} ++ {(- s)} by Th19 .= {(a - s),(b - s)} by Th52 ; ::_thesis: verum end; theorem :: MEMBER_1:78 for a, b, s, t being complex number holds {a,b} -- {s,t} = {(a - s),(a - t),(b - s),(b - t)} proof let a, b, s, t be complex number ; ::_thesis: {a,b} -- {s,t} = {(a - s),(a - t),(b - s),(b - t)} thus {a,b} -- {s,t} = {a,b} ++ {(- s),(- t)} by Th20 .= {(a - s),(a - t),(b - s),(b - t)} by Th53 ; ::_thesis: verum end; definition let F, G be ext-real-membered set ; funcF ** G -> set equals :: MEMBER_1:def 9 { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; coherence { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ; commutativity for b1 being set for F, G being ext-real-membered set st b1 = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds b1 = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } proof let X be set ; ::_thesis: for F, G being ext-real-membered set st X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } let F, G be ext-real-membered set ; ::_thesis: ( X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } implies X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ) assume A1: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } thus X c= { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ) assume e in X ; ::_thesis: e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } then ex w1, w2 being Element of ExtREAL st ( e = w1 * w2 & w1 in F & w2 in G ) by A1; hence e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } or e in X ) assume e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: e in X then ex w1, w2 being Element of ExtREAL st ( e = w1 * w2 & w1 in G & w2 in F ) ; hence e in X by A1; ::_thesis: verum 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 ; clusterF ** G -> empty ; coherence F ** G is empty proof assume not F ** G is empty ; ::_thesis: contradiction then the Element of F ** G in F ** G ; then ex w1, w2 being Element of ExtREAL st ( the Element of F ** G = w1 * w2 & w1 in F & w2 in G ) ; hence contradiction ; ::_thesis: verum end; clusterG ** F -> empty ; coherence G ** F is empty ; end; registration let F, G be ext-real-membered set ; clusterF ** G -> ext-real-membered ; coherence F ** G is ext-real-membered proof let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in F ** G or e is ext-real ) assume e in F ** G ; ::_thesis: e is ext-real then ex w1, w2 being Element of ExtREAL st ( e = w1 * w2 & w1 in F & w2 in G ) ; hence e is ext-real ; ::_thesis: verum end; end; theorem Th79: :: MEMBER_1:79 for F, G being ext-real-membered set for f, g being ext-real number st f in F & g in G holds f * g in F ** G proof let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds f * g in F ** G let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f * g in F ** G ) ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; hence ( f in F & g in G implies f * g in F ** G ) ; ::_thesis: verum end; registration let F, G be non empty ext-real-membered set ; clusterF ** G -> non empty ; coherence not F ** G is empty proof the Element of F * the Element of G in F ** G by Th79; hence not F ** G is empty ; ::_thesis: verum end; end; theorem Th80: :: MEMBER_1:80 for F, G, H being ext-real-membered set holds (F ** G) ** H = F ** (G ** H) proof let F, G, H be ext-real-membered set ; ::_thesis: (F ** G) ** H = F ** (G ** H) let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F ** G) ** H or i in F ** (G ** H) ) & ( not i in F ** (G ** H) or i in (F ** G) ** H ) ) hereby ::_thesis: ( not i in F ** (G ** H) or i in (F ** G) ** H ) assume i in (F ** G) ** H ; ::_thesis: i in F ** (G ** H) then consider w, w1 being Element of ExtREAL such that A1: i = w * w1 and A2: w in F ** G and A3: w1 in H ; consider w2, w3 being Element of ExtREAL such that A4: w = w2 * w3 and A5: w2 in F and A6: w3 in G by A2; ( i = w2 * (w3 * w1) & w3 * w1 in G ** H ) by A1, A3, A4, A6, XXREAL_3:66; hence i in F ** (G ** H) by A5; ::_thesis: verum end; assume i in F ** (G ** H) ; ::_thesis: i in (F ** G) ** H then consider w, w1 being Element of ExtREAL such that A7: ( i = w * w1 & w in F ) and A8: w1 in G ** H ; consider w2, w3 being Element of ExtREAL such that A9: ( w1 = w2 * w3 & w2 in G ) and A10: w3 in H by A8; ( i = (w * w2) * w3 & w * w2 in F ** G ) by A7, A9, XXREAL_3:66; hence i in (F ** G) ** H by A10; ::_thesis: verum 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 let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F ** H c= G ** I ) assume A1: ( F c= G & H c= I ) ; ::_thesis: F ** H c= G ** I let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F ** H or i in G ** I ) assume i in F ** H ; ::_thesis: i in G ** I then ex w, w1 being Element of ExtREAL st ( i = w * w1 & w in F & w1 in H ) ; hence i in G ** I by A1; ::_thesis: verum end; theorem Th82: :: MEMBER_1:82 for F, G, H being ext-real-membered set holds F ** (G \/ H) = (F ** G) \/ (F ** H) proof let F, G, H be ext-real-membered set ; ::_thesis: F ** (G \/ H) = (F ** G) \/ (F ** H) let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in F ** (G \/ H) or j in (F ** G) \/ (F ** H) ) & ( not j in (F ** G) \/ (F ** H) or j in F ** (G \/ H) ) ) hereby ::_thesis: ( not j in (F ** G) \/ (F ** H) or j in F ** (G \/ H) ) assume j in F ** (G \/ H) ; ::_thesis: j in (F ** G) \/ (F ** H) then consider w, w1 being Element of ExtREAL such that A1: j = w * w1 and A2: w in F and A3: w1 in G \/ H ; ( w1 in G or w1 in H ) by A3, XBOOLE_0:def_3; then ( w * w1 in F ** G or w * w1 in F ** H ) by A2; hence j in (F ** G) \/ (F ** H) by A1, XBOOLE_0:def_3; ::_thesis: verum end; assume A4: j in (F ** G) \/ (F ** H) ; ::_thesis: j in F ** (G \/ H) percases ( j in F ** G or j in F ** H ) by A4, XBOOLE_0:def_3; suppose j in F ** G ; ::_thesis: j in F ** (G \/ H) then consider w, w1 being Element of ExtREAL such that A5: ( j = w * w1 & w in F ) and A6: w1 in G ; w1 in G \/ H by A6, XBOOLE_0:def_3; hence j in F ** (G \/ H) by A5; ::_thesis: verum end; suppose j in F ** H ; ::_thesis: j in F ** (G \/ H) then consider w, w1 being Element of ExtREAL such that A7: ( j = w * w1 & w in F ) and A8: w1 in H ; w1 in G \/ H by A8, XBOOLE_0:def_3; hence j in F ** (G \/ H) by A7; ::_thesis: verum end; end; 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 let F, G, H be ext-real-membered set ; ::_thesis: F ** (G /\ H) c= (F ** G) /\ (F ** H) let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in F ** (G /\ H) or j in (F ** G) /\ (F ** H) ) assume j in F ** (G /\ H) ; ::_thesis: j in (F ** G) /\ (F ** H) then consider w, w1 being Element of ExtREAL such that A1: j = w * w1 and A2: w in F and A3: w1 in G /\ H ; w1 in H by A3, XBOOLE_0:def_4; then A4: w * w1 in F ** H by A2; w1 in G by A3, XBOOLE_0:def_4; then w * w1 in F ** G by A2; hence j in (F ** G) /\ (F ** H) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: MEMBER_1:84 for F, G being ext-real-membered set holds F ** (-- G) = -- (F ** G) proof let F, G be ext-real-membered set ; ::_thesis: F ** (-- G) = -- (F ** G) let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in F ** (-- G) or i in -- (F ** G) ) & ( not i in -- (F ** G) or i in F ** (-- G) ) ) hereby ::_thesis: ( not i in -- (F ** G) or i in F ** (-- G) ) assume i in F ** (-- G) ; ::_thesis: i in -- (F ** G) then consider w, w1 being Element of ExtREAL such that A1: i = w * w1 and A2: w in F and A3: w1 in -- G ; w * (- w1) = - (w * w1) by XXREAL_3:92; then A4: i = - (w * (- w1)) by A1; - w1 in G by A3, Th2; then w * (- w1) in F ** G by A2; hence i in -- (F ** G) by A4; ::_thesis: verum end; assume i in -- (F ** G) ; ::_thesis: i in F ** (-- G) then - i in F ** G by Th2; then consider w, w1 being Element of ExtREAL such that A5: ( - i = w * w1 & w in F ) and A6: w1 in G ; ( w * (- w1) = - (w * w1) & - w1 in -- G ) by A6, XXREAL_3:92; hence i in F ** (-- G) by A5; ::_thesis: verum end; theorem Th85: :: MEMBER_1:85 for F, G being ext-real-membered set holds (F ** G) "" = (F "") ** (G "") proof let F, G be ext-real-membered set ; ::_thesis: (F ** G) "" = (F "") ** (G "") let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F ** G) "" or i in (F "") ** (G "") ) & ( not i in (F "") ** (G "") or i in (F ** G) "" ) ) hereby ::_thesis: ( not i in (F "") ** (G "") or i in (F ** G) "" ) assume i in (F ** G) "" ; ::_thesis: i in (F "") ** (G "") then consider w being Element of ExtREAL such that A1: i = w " and A2: w in F ** G ; consider w1, w2 being Element of ExtREAL such that A3: w = w1 * w2 and A4: ( w1 in F & w2 in G ) by A2; A5: ( w1 " in F "" & w2 " in G "" ) by A4; i = (w1 ") * (w2 ") by A1, A3, XXREAL_3:67; hence i in (F "") ** (G "") by A5; ::_thesis: verum end; assume i in (F "") ** (G "") ; ::_thesis: i in (F ** G) "" then consider w, w1 being Element of ExtREAL such that A6: i = w * w1 and A7: w in F "" and A8: w1 in G "" ; consider w3 being Element of ExtREAL such that A9: w1 = w3 " and A10: w3 in G by A8; consider w2 being Element of ExtREAL such that A11: w = w2 " and A12: w2 in F by A7; A13: w2 * w3 in F ** G by A12, A10; i = (w2 * w3) " by A6, A11, A9, XXREAL_3:67; hence i in (F ** G) "" by A13; ::_thesis: verum end; theorem Th86: :: MEMBER_1:86 for f, g being ext-real number holds {f} ** {g} = {(f * g)} proof let f, g be ext-real number ; ::_thesis: {f} ** {g} = {(f * g)} let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in {f} ** {g} or i in {(f * g)} ) & ( not i in {(f * g)} or i in {f} ** {g} ) ) hereby ::_thesis: ( not i in {(f * g)} or i in {f} ** {g} ) assume i in {f} ** {g} ; ::_thesis: i in {(f * g)} then consider w1, w2 being Element of ExtREAL such that A1: i = w1 * w2 and A2: ( w1 in {f} & w2 in {g} ) ; ( w1 = f & w2 = g ) by A2, TARSKI:def_1; hence i in {(f * g)} by A1, TARSKI:def_1; ::_thesis: verum end; A3: ( f in {f} & g in {g} ) by TARSKI:def_1; assume i in {(f * g)} ; ::_thesis: i in {f} ** {g} then A4: i = f * g by TARSKI:def_1; ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; hence i in {f} ** {g} by A4, A3; ::_thesis: verum end; theorem Th87: :: MEMBER_1:87 for f, h, i being ext-real number holds {f} ** {h,i} = {(f * h),(f * i)} proof let f, h, i be ext-real number ; ::_thesis: {f} ** {h,i} = {(f * h),(f * i)} thus {f} ** {h,i} = {f} ** ({h} \/ {i}) by ENUMSET1:1 .= ({f} ** {h}) \/ ({f} ** {i}) by Th82 .= {(f * h)} \/ ({f} ** {i}) by Th86 .= {(f * h)} \/ {(f * i)} by Th86 .= {(f * h),(f * i)} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th88: :: MEMBER_1:88 for f, g, h, i being ext-real number holds {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)} proof let f, g, h, i be ext-real number ; ::_thesis: {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)} thus {f,g} ** {h,i} = ({f} \/ {g}) ** {h,i} by ENUMSET1:1 .= ({f} ** {h,i}) \/ ({g} ** {h,i}) by Th82 .= {(f * h),(f * i)} \/ ({g} ** {h,i}) by Th87 .= {(f * h),(f * i)} \/ {(g * h),(g * i)} by Th87 .= {(f * h),(f * i),(g * h),(g * i)} by ENUMSET1:5 ; ::_thesis: verum end; definition let A, B be complex-membered set ; funcA ** B -> set equals :: MEMBER_1:def 10 { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; coherence { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ; commutativity for b1 being set for A, B being complex-membered set st b1 = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds b1 = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } proof let X be set ; ::_thesis: for A, B being complex-membered set st X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } let A, B be complex-membered set ; ::_thesis: ( X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } implies X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ) assume A1: X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } thus X c= { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ) assume e in X ; ::_thesis: e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) by A1; hence e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } or e in X ) assume e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: e in X then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in B & c2 in A ) ; hence e in X by A1; ::_thesis: verum end; end; :: deftheorem defines ** MEMBER_1:def_10_:_ for A, B being complex-membered set holds A ** B = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; theorem Th89: :: MEMBER_1:89 for A, B being complex-membered set for a, b being complex number st a in A & b in B holds a * b in A ** B proof let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds a * b in A ** B let a, b be complex number ; ::_thesis: ( a in A & b in B implies a * b in A ** B ) ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; hence ( a in A & b in B implies a * b in A ** B ) ; ::_thesis: verum end; registration let A be empty set ; let B be complex-membered set ; clusterA ** B -> empty ; coherence A ** B is empty proof assume not A ** B is empty ; ::_thesis: contradiction then the Element of A ** B in A ** B ; then ex c1, c2 being Element of COMPLEX st ( the Element of A ** B = c1 * c2 & c1 in A & c2 in B ) ; hence contradiction ; ::_thesis: verum end; clusterB ** A -> empty ; coherence B ** A is empty ; end; registration let A, B be non empty complex-membered set ; clusterA ** B -> non empty ; coherence not A ** B is empty proof the Element of A * the Element of B in A ** B by Th89; hence not A ** B is empty ; ::_thesis: verum end; end; registration let A, B be complex-membered set ; clusterA ** B -> complex-membered ; coherence A ** B is complex-membered proof let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in A ** B or e is complex ) assume e in A ** B ; ::_thesis: e is complex then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) ; hence e is complex ; ::_thesis: verum end; end; registration let A, B be real-membered set ; clusterA ** B -> real-membered ; coherence A ** B is real-membered proof let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A ** B or e is real ) assume e in A ** B ; ::_thesis: e is real then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) ; hence e is real ; ::_thesis: verum end; end; registration let A, B be rational-membered set ; clusterA ** B -> rational-membered ; coherence A ** B is rational-membered proof let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A ** B or e is rational ) assume e in A ** B ; ::_thesis: e is rational then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) ; hence e is rational ; ::_thesis: verum end; end; registration let A, B be integer-membered set ; clusterA ** B -> integer-membered ; coherence A ** B is integer-membered proof let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in A ** B or e is integer ) assume e in A ** B ; ::_thesis: e is integer then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) ; hence e is integer ; ::_thesis: verum end; end; registration let A, B be natural-membered set ; clusterA ** B -> natural-membered ; coherence A ** B is natural-membered proof let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( not e in A ** B or e is natural ) assume e in A ** B ; ::_thesis: e is natural then ex c1, c2 being Element of COMPLEX st ( e = c1 * c2 & c1 in A & c2 in B ) ; hence e is natural ; ::_thesis: verum end; end; registration let A, B be real-membered set ; let F, G be ext-real-membered set ; identifyA ** B with F ** G when A = F, B = G; compatibility ( A = F & B = G implies A ** B = F ** G ) proof assume A1: ( A = F & B = G ) ; ::_thesis: A ** B = F ** G let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A ** B or a in F ** G ) & ( not a in F ** G or a in A ** B ) ) hereby ::_thesis: ( not a in F ** G or a in A ** B ) assume a in A ** B ; ::_thesis: a in F ** G then consider c, c1 being Element of COMPLEX such that A2: a = c * c1 and A3: ( c in A & c1 in B ) ; reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def_1; a = d1 * d2 by A2, A3, XXREAL_3:def_5; hence a in F ** G by A1, A3; ::_thesis: verum end; assume a in F ** G ; ::_thesis: a in A ** B then consider w, w1 being Element of ExtREAL such that A4: a = w * w1 and A5: ( w in F & w1 in G ) ; reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def_2; a = d1 * d2 by A1, A4, A5, XXREAL_3:def_5; hence a in A ** B by A1, A5; ::_thesis: verum end; end; theorem Th90: :: MEMBER_1:90 for A, B, C being complex-membered set holds (A ** B) ** C = A ** (B ** C) proof let A, B, C be complex-membered set ; ::_thesis: (A ** B) ** C = A ** (B ** C) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ** B) ** C or a in A ** (B ** C) ) & ( not a in A ** (B ** C) or a in (A ** B) ** C ) ) hereby ::_thesis: ( not a in A ** (B ** C) or a in (A ** B) ** C ) assume a in (A ** B) ** C ; ::_thesis: a in A ** (B ** C) then consider c, c1 being Element of COMPLEX such that A1: a = c * c1 and A2: c in A ** B and A3: c1 in C ; consider c2, c3 being Element of COMPLEX such that A4: c = c2 * c3 and A5: c2 in A and A6: c3 in B by A2; ( a = c2 * (c3 * c1) & c3 * c1 in B ** C ) by A1, A3, A4, A6; hence a in A ** (B ** C) by A5; ::_thesis: verum end; assume a in A ** (B ** C) ; ::_thesis: a in (A ** B) ** C then consider c, c1 being Element of COMPLEX such that A7: ( a = c * c1 & c in A ) and A8: c1 in B ** C ; consider c2, c3 being Element of COMPLEX such that A9: ( c1 = c2 * c3 & c2 in B ) and A10: c3 in C by A8; ( a = (c * c2) * c3 & c * c2 in A ** B ) by A7, A9; hence a in (A ** B) ** C by A10; ::_thesis: verum 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 let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A ** C c= B ** D ) assume A1: ( A c= B & C c= D ) ; ::_thesis: A ** C c= B ** D let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** C or a in B ** D ) assume a in A ** C ; ::_thesis: a in B ** D then ex c, c1 being Element of COMPLEX st ( a = c * c1 & c in A & c1 in C ) ; hence a in B ** D by A1; ::_thesis: verum end; theorem Th92: :: MEMBER_1:92 for A, B, C being complex-membered set holds A ** (B \/ C) = (A ** B) \/ (A ** C) proof let A, B, C be complex-membered set ; ::_thesis: A ** (B \/ C) = (A ** B) \/ (A ** C) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ** (B \/ C) or a in (A ** B) \/ (A ** C) ) & ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) ) ) hereby ::_thesis: ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) ) assume a in A ** (B \/ C) ; ::_thesis: a in (A ** B) \/ (A ** C) then consider c, c1 being Element of COMPLEX such that A1: a = c * c1 and A2: c in A and A3: c1 in B \/ C ; ( c1 in B or c1 in C ) by A3, XBOOLE_0:def_3; then ( c * c1 in A ** B or c * c1 in A ** C ) by A2; hence a in (A ** B) \/ (A ** C) by A1, XBOOLE_0:def_3; ::_thesis: verum end; assume A4: a in (A ** B) \/ (A ** C) ; ::_thesis: a in A ** (B \/ C) percases ( a in A ** B or a in A ** C ) by A4, XBOOLE_0:def_3; suppose a in A ** B ; ::_thesis: a in A ** (B \/ C) then consider c, c1 being Element of COMPLEX such that A5: ( a = c * c1 & c in A ) and A6: c1 in B ; c1 in B \/ C by A6, XBOOLE_0:def_3; hence a in A ** (B \/ C) by A5; ::_thesis: verum end; suppose a in A ** C ; ::_thesis: a in A ** (B \/ C) then consider c, c1 being Element of COMPLEX such that A7: ( a = c * c1 & c in A ) and A8: c1 in C ; c1 in B \/ C by A8, XBOOLE_0:def_3; hence a in A ** (B \/ C) by A7; ::_thesis: verum end; end; end; theorem Th93: :: MEMBER_1:93 for A, B, C being complex-membered set holds A ** (B /\ C) c= (A ** B) /\ (A ** C) proof let A, B, C be complex-membered set ; ::_thesis: A ** (B /\ C) c= (A ** B) /\ (A ** C) let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** (B /\ C) or a in (A ** B) /\ (A ** C) ) assume a in A ** (B /\ C) ; ::_thesis: a in (A ** B) /\ (A ** C) then consider c, c1 being Element of COMPLEX such that A1: a = c * c1 and A2: c in A and A3: c1 in B /\ C ; c1 in C by A3, XBOOLE_0:def_4; then A4: c * c1 in A ** C by A2; c1 in B by A3, XBOOLE_0:def_4; then c * c1 in A ** B by A2; hence a in (A ** B) /\ (A ** C) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th94: :: MEMBER_1:94 for A, B being complex-membered set holds A ** (-- B) = -- (A ** B) proof let A, B be complex-membered set ; ::_thesis: A ** (-- B) = -- (A ** B) let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ** (-- B) or a in -- (A ** B) ) & ( not a in -- (A ** B) or a in A ** (-- B) ) ) hereby ::_thesis: ( not a in -- (A ** B) or a in A ** (-- B) ) assume a in A ** (-- B) ; ::_thesis: a in -- (A ** B) then consider c, c1 being Element of COMPLEX such that A1: a = c * c1 and A2: c in A and A3: c1 in -- B ; - c1 in B by A3, Th12; then A4: c * (- c1) in A ** B by A2; a = - (c * (- c1)) by A1; hence a in -- (A ** B) by A4; ::_thesis: verum end; assume a in -- (A ** B) ; ::_thesis: a in A ** (-- B) then - a in A ** B by Th12; then consider c, c1 being Element of COMPLEX such that A5: - a = c * c1 and A6: c in A and A7: c1 in B ; ( a = c * (- c1) & - c1 in -- B ) by A5, A7; hence a in A ** (-- B) by A6; ::_thesis: verum end; theorem Th95: :: MEMBER_1:95 for A, B, C being complex-membered set holds A ** (B ++ C) c= (A ** B) ++ (A ** C) proof let A, B, C be complex-membered set ; ::_thesis: A ** (B ++ C) c= (A ** B) ++ (A ** C) let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** (B ++ C) or a in (A ** B) ++ (A ** C) ) assume a in A ** (B ++ C) ; ::_thesis: a in (A ** B) ++ (A ** C) then consider c, c1 being Element of COMPLEX such that A1: a = c * c1 and A2: c in A and A3: c1 in B ++ C ; consider c2, c3 being Element of COMPLEX such that A4: ( c1 = c2 + c3 & c2 in B ) and A5: c3 in C by A3; A6: c * c3 in A ** C by A2, A5; ( a = (c * c2) + (c * c3) & c * c2 in A ** B ) by A1, A2, A4; hence a in (A ** B) ++ (A ** C) by A6; ::_thesis: verum end; theorem Th96: :: MEMBER_1:96 for A, B, C being complex-membered set holds A ** (B -- C) c= (A ** B) -- (A ** C) proof let A, B, C be complex-membered set ; ::_thesis: A ** (B -- C) c= (A ** B) -- (A ** C) A ** (B ++ (-- C)) c= (A ** B) ++ (A ** (-- C)) by Th95; hence A ** (B -- C) c= (A ** B) -- (A ** C) by Th94; ::_thesis: verum end; theorem Th97: :: MEMBER_1:97 for A, B being complex-membered set holds (A ** B) "" = (A "") ** (B "") proof let A, B be complex-membered set ; ::_thesis: (A ** B) "" = (A "") ** (B "") let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ** B) "" or a in (A "") ** (B "") ) & ( not a in (A "") ** (B "") or a in (A ** B) "" ) ) hereby ::_thesis: ( not a in (A "") ** (B "") or a in (A ** B) "" ) assume a in (A ** B) "" ; ::_thesis: a in (A "") ** (B "") then consider c being Element of COMPLEX such that A1: a = c " and A2: c in A ** B ; consider c1, c2 being Element of COMPLEX such that A3: c = c1 * c2 and A4: ( c1 in A & c2 in B ) by A2; A5: ( c1 " in A "" & c2 " in B "" ) by A4; a = (c1 ") * (c2 ") by A1, A3, XCMPLX_1:204; hence a in (A "") ** (B "") by A5; ::_thesis: verum end; assume a in (A "") ** (B "") ; ::_thesis: a in (A ** B) "" then consider c, c1 being Element of COMPLEX such that A6: a = c * c1 and A7: c in A "" and A8: c1 in B "" ; consider c3 being Element of COMPLEX such that A9: c1 = c3 " and A10: c3 in B by A8; consider c2 being Element of COMPLEX such that A11: c = c2 " and A12: c2 in A by A7; A13: c2 * c3 in A ** B by A12, A10; a = (c2 * c3) " by A6, A11, A9, XCMPLX_1:204; hence a in (A ** B) "" by A13; ::_thesis: verum end; theorem Th98: :: MEMBER_1:98 for a, b being complex number holds {a} ** {b} = {(a * b)} proof let a, b be complex number ; ::_thesis: {a} ** {b} = {(a * b)} let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} ** {b} or z in {(a * b)} ) & ( not z in {(a * b)} or z in {a} ** {b} ) ) hereby ::_thesis: ( not z in {(a * b)} or z in {a} ** {b} ) assume z in {a} ** {b} ; ::_thesis: z in {(a * b)} then consider c1, c2 being Element of COMPLEX such that A1: z = c1 * c2 and A2: ( c1 in {a} & c2 in {b} ) ; ( c1 = a & c2 = b ) by A2, TARSKI:def_1; hence z in {(a * b)} by A1, TARSKI:def_1; ::_thesis: verum end; A3: ( a in {a} & b in {b} ) by TARSKI:def_1; assume z in {(a * b)} ; ::_thesis: z in {a} ** {b} then A4: z = a * b by TARSKI:def_1; ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; hence z in {a} ** {b} by A4, A3; ::_thesis: verum end; theorem Th99: :: MEMBER_1:99 for a, s, t being complex number holds {a} ** {s,t} = {(a * s),(a * t)} proof let a, s, t be complex number ; ::_thesis: {a} ** {s,t} = {(a * s),(a * t)} thus {a} ** {s,t} = {a} ** ({s} \/ {t}) by ENUMSET1:1 .= ({a} ** {s}) \/ ({a} ** {t}) by Th92 .= {(a * s)} \/ ({a} ** {t}) by Th98 .= {(a * s)} \/ {(a * t)} by Th98 .= {(a * s),(a * t)} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th100: :: MEMBER_1:100 for a, b, s, t being complex number holds {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)} proof let a, b, s, t be complex number ; ::_thesis: {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)} thus {a,b} ** {s,t} = ({a} \/ {b}) ** {s,t} by ENUMSET1:1 .= ({a} ** {s,t}) \/ ({b} ** {s,t}) by Th92 .= {(a * s),(a * t)} \/ ({b} ** {s,t}) by Th99 .= {(a * s),(a * t)} \/ {(b * s),(b * t)} by Th99 .= {(a * s),(a * t),(b * s),(b * t)} by ENUMSET1:5 ; ::_thesis: verum end; definition let F, G be ext-real-membered set ; funcF /// G -> set equals :: MEMBER_1:def 11 F ** (G ""); coherence F ** (G "") is set ; end; :: deftheorem defines /// MEMBER_1:def_11_:_ for F, G being ext-real-membered set holds F /// G = F ** (G ""); theorem Th101: :: MEMBER_1:101 for F, G being ext-real-membered set holds F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } proof let F, G be ext-real-membered set ; ::_thesis: F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } thus F /// G c= { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F /// G proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F /// G or e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ) assume e in F /// G ; ::_thesis: e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 * w2 and A2: w1 in F and A3: w2 in G "" ; consider w being Element of ExtREAL such that A4: w2 = w " and A5: w in G by A3; e = w1 / w by A1, A4; hence e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A2, A5; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } or e in F /// G ) assume e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: e in F /// G then consider w1, w2 being Element of ExtREAL such that A6: ( e = w1 / w2 & w1 in F ) and A7: w2 in G ; w2 " in G "" by A7; hence e in F /// G by A6; ::_thesis: verum end; theorem Th102: :: MEMBER_1:102 for F, G being ext-real-membered set for f, g being ext-real number st f in F & g in G holds f / g in F /// G proof let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds f / g in F /// G let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f / g in F /// G ) A1: ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1; F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by Th101; hence ( f in F & g in G implies f / g in F /// G ) by A1; ::_thesis: verum end; registration let F be empty set ; let G be ext-real-membered set ; clusterF /// G -> empty ; coherence F /// G is empty ; clusterG /// F -> empty ; coherence G /// F is empty ; end; registration let F, G be non empty ext-real-membered set ; clusterF /// G -> non empty ; coherence not F /// G is empty ; end; registration let F, G be ext-real-membered set ; clusterF /// G -> ext-real-membered ; coherence F /// G is ext-real-membered ; end; theorem :: MEMBER_1:103 for F, G, H, I being ext-real-membered set st F c= G & H c= I holds F /// H c= G /// I proof let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F /// H c= G /// I ) assume A1: ( F c= G & H c= I ) ; ::_thesis: F /// H c= G /// I let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F /// H or i in G /// I ) A2: F /// H = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th101; assume i in F /// H ; ::_thesis: i in G /// I then ex w, w1 being Element of ExtREAL st ( i = w / w1 & w in F & w1 in H ) by A2; hence i in G /// I by A1, Th102; ::_thesis: verum 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 let F, G, H be ext-real-membered set ; ::_thesis: F /// (G \/ H) = (F /// G) \/ (F /// H) thus F /// (G \/ H) = F ** ((G "") \/ (H "")) by Th23 .= (F /// G) \/ (F /// H) by Th82 ; ::_thesis: verum end; theorem :: MEMBER_1:107 for F, G, H being ext-real-membered set holds F /// (G /\ H) c= (F /// G) /\ (F /// H) proof let F, G, H be ext-real-membered set ; ::_thesis: F /// (G /\ H) c= (F /// G) /\ (F /// H) (G /\ H) "" c= (G "") /\ (H "") by Th24; then A1: F ** ((G /\ H) "") c= F ** ((G "") /\ (H "")) by Th81; F ** ((G "") /\ (H "")) c= (F ** (G "")) /\ (F ** (H "")) by Th83; hence F /// (G /\ H) c= (F /// G) /\ (F /// H) by A1, XBOOLE_1:1; ::_thesis: verum 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 let F, G, H be ext-real-membered set ; ::_thesis: (F /// G) /// H = F /// (G ** H) thus (F /// G) /// H = F ** ((G "") ** (H "")) by Th80 .= F /// (G ** H) by Th85 ; ::_thesis: verum end; theorem :: MEMBER_1:111 for f, g being ext-real number holds {f} /// {g} = {(f / g)} proof let f, g be ext-real number ; ::_thesis: {f} /// {g} = {(f / g)} thus {f} /// {g} = {f} ** {(g ")} by Th26 .= {(f / g)} by Th86 ; ::_thesis: verum end; theorem :: MEMBER_1:112 for f, h, i being ext-real number holds {f} /// {h,i} = {(f / h),(f / i)} proof let f, h, i be ext-real number ; ::_thesis: {f} /// {h,i} = {(f / h),(f / i)} thus {f} /// {h,i} = {f} ** {(h "),(i ")} by Th27 .= {(f / h),(f / i)} by Th87 ; ::_thesis: verum end; theorem :: MEMBER_1:113 for f, g, h being ext-real number holds {f,g} /// {h} = {(f / h),(g / h)} proof let f, g, h be ext-real number ; ::_thesis: {f,g} /// {h} = {(f / h),(g / h)} thus {f,g} /// {h} = {f,g} ** {(h ")} by Th26 .= {(f / h),(g / h)} by Th87 ; ::_thesis: verum end; theorem :: MEMBER_1:114 for f, g, h, i being ext-real number holds {f,g} /// {h,i} = {(f / h),(f / i),(g / h),(g / i)} proof let f, g, h, i be ext-real number ; ::_thesis: {f,g} /// {h,i} = {(f / h),(f / i),(g / h),(g / i)} thus {f,g} /// {h,i} = {f,g} ** {(h "),(i ")} by Th27 .= {(f / h),(f / i),(g / h),(g / i)} by Th88 ; ::_thesis: verum end; definition let A, B be complex-membered set ; funcA /// B -> set equals :: MEMBER_1:def 12 A ** (B ""); coherence A ** (B "") is set ; end; :: deftheorem defines /// MEMBER_1:def_12_:_ for A, B being complex-membered set holds A /// B = A ** (B ""); theorem Th115: :: MEMBER_1:115 for A, B being complex-membered set holds A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } proof let A, B be complex-membered set ; ::_thesis: A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } thus A /// B c= { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } c= A /// B proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A /// B or e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ) assume e in A /// B ; ::_thesis: e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } then consider c1, c2 being Element of COMPLEX such that A1: e = c1 * c2 and A2: c1 in A and A3: c2 in B "" ; ( e = c1 / (c2 ") & c2 " in B ) by A1, A3, Th29; hence e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by A2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } or e in A /// B ) assume e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: e in A /// B then consider c1, c2 being Element of COMPLEX such that A4: ( e = c1 / c2 & c1 in A ) and A5: c2 in B ; c2 " in B "" by A5; hence e in A /// B by A4; ::_thesis: verum end; theorem Th116: :: MEMBER_1:116 for A, B being complex-membered set for a, b being complex number st a in A & b in B holds a / b in A /// B proof let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds a / b in A /// B let a, b be complex number ; ::_thesis: ( a in A & b in B implies a / b in A /// B ) A1: ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2; A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by Th115; hence ( a in A & b in B implies a / b in A /// B ) by A1; ::_thesis: verum end; registration let A be empty set ; let B be complex-membered set ; clusterA /// B -> empty ; coherence A /// B is empty ; clusterB /// A -> empty ; coherence B /// A is empty ; end; registration let A, B be non empty complex-membered set ; clusterA /// B -> non empty ; coherence not A /// B is empty ; end; registration let A, B be complex-membered set ; clusterA /// B -> complex-membered ; coherence A /// B is complex-membered ; end; registration let A, B be real-membered set ; clusterA /// B -> real-membered ; coherence A /// B is real-membered ; end; registration let A, B be rational-membered set ; clusterA /// B -> rational-membered ; coherence A /// B is rational-membered ; end; registration let A, B be real-membered set ; let F, G be ext-real-membered set ; identifyA /// B with F /// G when A = F, B = G; compatibility ( A = F & B = G implies A /// B = F /// G ) ; end; theorem :: MEMBER_1:117 for A, B, C, D being complex-membered set st A c= B & C c= D holds A /// C c= B /// D proof let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A /// C c= B /// D ) assume A1: ( A c= B & C c= D ) ; ::_thesis: A /// C c= B /// D let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A /// C or z in B /// D ) A2: A /// C = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in C ) } by Th115; assume z in A /// C ; ::_thesis: z in B /// D then ex c, c1 being Element of COMPLEX st ( z = c / c1 & c in A & c1 in C ) by A2; hence z in B /// D by A1, Th116; ::_thesis: verum end; theorem :: MEMBER_1:118 for A, B, C being complex-membered set holds A /// (B \/ C) = (A /// B) \/ (A /// C) proof let A, B, C be complex-membered set ; ::_thesis: A /// (B \/ C) = (A /// B) \/ (A /// C) thus A /// (B \/ C) = A ** ((B "") \/ (C "")) by Th32 .= (A /// B) \/ (A /// C) by Th92 ; ::_thesis: verum end; theorem :: MEMBER_1:119 for A, B, C being complex-membered set holds A /// (B /\ C) c= (A /// B) /\ (A /// C) proof let A, B, C be complex-membered set ; ::_thesis: A /// (B /\ C) c= (A /// B) /\ (A /// C) A /// (B /\ C) = A ** ((B "") /\ (C "")) by Th33; hence A /// (B /\ C) c= (A /// B) /\ (A /// C) by Th93; ::_thesis: verum end; theorem :: MEMBER_1:120 for A, B being complex-membered set holds A /// (-- B) = -- (A /// B) proof let A, B be complex-membered set ; ::_thesis: A /// (-- B) = -- (A /// B) thus A /// (-- B) = A ** (-- (B "")) by Th36 .= -- (A /// B) by Th94 ; ::_thesis: verum 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 let A, B, C be complex-membered set ; ::_thesis: (A -- B) /// C c= (A /// C) -- (B /// C) (A ++ (-- B)) /// C c= (A /// C) ++ ((-- B) /// C) by Th95; hence (A -- B) /// C c= (A /// C) -- (B /// C) by Th94; ::_thesis: verum 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 let A, B, C be complex-membered set ; ::_thesis: (A /// B) /// C = A /// (B ** C) thus (A /// B) /// C = A ** ((B "") ** (C "")) by Th90 .= A /// (B ** C) by Th97 ; ::_thesis: verum end; theorem :: MEMBER_1:127 for A, B, C being complex-membered set holds A /// (B /// C) = (A ** C) /// B proof let A, B, C be complex-membered set ; ::_thesis: A /// (B /// C) = (A ** C) /// B thus A /// (B /// C) = A ** ((B "") ** ((C "") "")) by Th97 .= (A ** C) /// B by Th90 ; ::_thesis: verum end; theorem :: MEMBER_1:128 for a, b being complex number holds {a} /// {b} = {(a / b)} proof let a, b be complex number ; ::_thesis: {a} /// {b} = {(a / b)} thus {a} /// {b} = {a} ** {(b ")} by Th37 .= {(a / b)} by Th98 ; ::_thesis: verum end; theorem :: MEMBER_1:129 for a, s, t being complex number holds {a} /// {s,t} = {(a / s),(a / t)} proof let a, s, t be complex number ; ::_thesis: {a} /// {s,t} = {(a / s),(a / t)} thus {a} /// {s,t} = {a} ** {(s "),(t ")} by Th38 .= {(a / s),(a / t)} by Th99 ; ::_thesis: verum end; theorem :: MEMBER_1:130 for a, b, s being complex number holds {a,b} /// {s} = {(a / s),(b / s)} proof let a, b, s be complex number ; ::_thesis: {a,b} /// {s} = {(a / s),(b / s)} thus {a,b} /// {s} = {a,b} ** {(s ")} by Th37 .= {(a / s),(b / s)} by Th99 ; ::_thesis: verum end; theorem :: MEMBER_1:131 for a, b, s, t being complex number holds {a,b} /// {s,t} = {(a / s),(a / t),(b / s),(b / t)} proof let a, b, s, t be complex number ; ::_thesis: {a,b} /// {s,t} = {(a / s),(a / t),(b / s),(b / t)} thus {a,b} /// {s,t} = {a,b} ** {(s "),(t ")} by Th38 .= {(a / s),(a / t),(b / s),(b / t)} by Th100 ; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcf ++ F -> set equals :: MEMBER_1:def 13 {f} ++ F; coherence {f} ++ F is set ; end; :: deftheorem defines ++ MEMBER_1:def_13_:_ for F being ext-real-membered set for f being ext-real number holds f ++ F = {f} ++ F; theorem Th132: :: MEMBER_1:132 for G being ext-real-membered set for g, f being ext-real number st g in G holds f + g in f ++ G proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds f + g in f ++ G let g, f be ext-real number ; ::_thesis: ( g in G implies f + g in f ++ G ) f in {f} by TARSKI:def_1; hence ( g in G implies f + g in f ++ G ) by Th39; ::_thesis: verum end; theorem Th133: :: MEMBER_1:133 for F being ext-real-membered set for f being ext-real number holds f ++ F = { (f + w) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f ++ F = { (f + w) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: f ++ F = { (f + w) where w is Element of ExtREAL : w in F } thus f ++ F c= { (f + w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f + w) where w is Element of ExtREAL : w in F } c= f ++ F proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f ++ F or e in { (f + w) where w is Element of ExtREAL : w in F } ) assume e in f ++ F ; ::_thesis: e in { (f + w) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 + w2 and A2: w1 in {f} and A3: w2 in F ; w1 = f by A2, TARSKI:def_1; hence e in { (f + w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f + w) where w is Element of ExtREAL : w in F } or e in f ++ F ) assume e in { (f + w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f ++ F then ex w being Element of ExtREAL st ( e = f + w & w in F ) ; hence e in f ++ F by Th132; ::_thesis: verum end; theorem Th134: :: MEMBER_1:134 for F being ext-real-membered set for f being ext-real number for e being set st e in f ++ F holds ex w being Element of ExtREAL st ( e = f + w & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in f ++ F holds ex w being Element of ExtREAL st ( e = f + w & w in F ) let e be set ; ::_thesis: ( e in f ++ F implies ex w being Element of ExtREAL st ( e = f + w & w in F ) ) f ++ F = { (f + w) where w is Element of ExtREAL : w in F } by Th133; hence ( e in f ++ F implies ex w being Element of ExtREAL st ( e = f + w & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterf ++ F -> empty ; coherence f ++ F is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterf ++ F -> non empty ; coherence not f ++ F is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterf ++ F -> ext-real-membered ; coherence f ++ F is ext-real-membered ; end; theorem Th135: :: MEMBER_1:135 for F, G being ext-real-membered set for r being real number st r ++ F c= r ++ G holds F c= G proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r ++ F c= r ++ G holds F c= G let r be real number ; ::_thesis: ( r ++ F c= r ++ G implies F c= G ) assume A1: r ++ F c= r ++ G ; ::_thesis: F c= G let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F or i in G ) assume i in F ; ::_thesis: i in G then r + i in r ++ F by Th132; then ex w being Element of ExtREAL st ( r + i = r + w & w in G ) by A1, Th134; hence i in G by XXREAL_3:11; ::_thesis: verum end; theorem :: MEMBER_1:136 for F, G being ext-real-membered set for r being real number st r ++ F = r ++ G holds F = G proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r ++ F = r ++ G holds F = G let r be real number ; ::_thesis: ( r ++ F = r ++ G implies F = G ) assume r ++ F = r ++ G ; ::_thesis: F = G then ( F c= G & G c= F ) by Th135; hence F = G by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th137: :: MEMBER_1:137 for F, G being ext-real-membered set for r being real number holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G) let r be real number ; ::_thesis: r ++ (F /\ G) = (r ++ F) /\ (r ++ G) A1: (r ++ F) /\ (r ++ G) c= r ++ (F /\ G) proof let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in (r ++ F) /\ (r ++ G) or j in r ++ (F /\ G) ) assume A2: j in (r ++ F) /\ (r ++ G) ; ::_thesis: j in r ++ (F /\ G) then j in r ++ F by XBOOLE_0:def_4; then consider w being Element of ExtREAL such that A3: j = r + w and A4: w in F by Th134; j in r ++ G by A2, XBOOLE_0:def_4; then consider w1 being Element of ExtREAL such that A5: j = r + w1 and A6: w1 in G by Th134; w = w1 by A3, A5, XXREAL_3:11; then w in F /\ G by A4, A6, XBOOLE_0:def_4; hence j in r ++ (F /\ G) by A3, Th132; ::_thesis: verum end; r ++ (F /\ G) c= (r ++ F) /\ (r ++ G) by Th42; hence r ++ (F /\ G) = (r ++ F) /\ (r ++ G) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th138: :: MEMBER_1:138 for F, G being ext-real-membered set for f being ext-real number holds (f ++ F) \ (f ++ G) c= f ++ (F \ G) proof let F, G be ext-real-membered set ; ::_thesis: for f being ext-real number holds (f ++ F) \ (f ++ G) c= f ++ (F \ G) let f be ext-real number ; ::_thesis: (f ++ F) \ (f ++ G) c= f ++ (F \ G) let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (f ++ F) \ (f ++ G) or i in f ++ (F \ G) ) assume A1: i in (f ++ F) \ (f ++ G) ; ::_thesis: i in f ++ (F \ G) then consider w being Element of ExtREAL such that A2: i = f + w and A3: w in F by Th134; now__::_thesis:_w_in_F_\_G assume not w in F \ G ; ::_thesis: contradiction then w in G by A3, XBOOLE_0:def_5; then f + w in f ++ G by Th132; hence contradiction by A1, A2, XBOOLE_0:def_5; ::_thesis: verum end; hence i in f ++ (F \ G) by A2, Th132; ::_thesis: verum end; theorem Th139: :: MEMBER_1:139 for F, G being ext-real-membered set for r being real number holds r ++ (F \ G) = (r ++ F) \ (r ++ G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F \ G) = (r ++ F) \ (r ++ G) let r be real number ; ::_thesis: r ++ (F \ G) = (r ++ F) \ (r ++ G) A1: r ++ (F \ G) c= (r ++ F) \ (r ++ G) proof let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in r ++ (F \ G) or i in (r ++ F) \ (r ++ G) ) assume i in r ++ (F \ G) ; ::_thesis: i in (r ++ F) \ (r ++ G) then consider w being Element of ExtREAL such that A2: i = r + w and A3: w in F \ G by Th134; A4: now__::_thesis:_not_r_+_w_in_r_++_G assume r + w in r ++ G ; ::_thesis: contradiction then consider w1 being Element of ExtREAL such that A5: r + w = r + w1 and A6: w1 in G by Th134; w = w1 by A5, XXREAL_3:11; hence contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum end; r + w in r ++ F by A3, Th132; hence i in (r ++ F) \ (r ++ G) by A2, A4, XBOOLE_0:def_5; ::_thesis: verum end; (r ++ F) \ (r ++ G) c= r ++ (F \ G) by Th138; hence r ++ (F \ G) = (r ++ F) \ (r ++ G) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th140: :: MEMBER_1:140 for F, G being ext-real-membered set for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G) let r be real number ; ::_thesis: r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G) thus r ++ (F \+\ G) = (r ++ (F \ G)) \/ (r ++ (G \ F)) by Th41 .= ((r ++ F) \ (r ++ G)) \/ (r ++ (G \ F)) by Th139 .= (r ++ F) \+\ (r ++ G) by Th139 ; ::_thesis: verum end; definition let A be complex-membered set ; let a be complex number ; funca ++ A -> set equals :: MEMBER_1:def 14 {a} ++ A; coherence {a} ++ A is set ; end; :: deftheorem defines ++ MEMBER_1:def_14_:_ for A being complex-membered set for a being complex number holds a ++ A = {a} ++ A; theorem Th141: :: MEMBER_1:141 for A being complex-membered set for b, a being complex number st b in A holds a + b in a ++ A proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds a + b in a ++ A let b, a be complex number ; ::_thesis: ( b in A implies a + b in a ++ A ) a in {a} by TARSKI:def_1; hence ( b in A implies a + b in a ++ A ) by Th46; ::_thesis: verum end; theorem Th142: :: MEMBER_1:142 for A being complex-membered set for a being complex number holds a ++ A = { (a + c) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds a ++ A = { (a + c) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: a ++ A = { (a + c) where c is Element of COMPLEX : c in A } thus a ++ A c= { (a + c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a + c) where c is Element of COMPLEX : c in A } c= a ++ A proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a ++ A or e in { (a + c) where c is Element of COMPLEX : c in A } ) assume e in a ++ A ; ::_thesis: e in { (a + c) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A1: e = c1 + c2 and A2: c1 in {a} and A3: c2 in A ; c1 = a by A2, TARSKI:def_1; hence e in { (a + c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a + c) where c is Element of COMPLEX : c in A } or e in a ++ A ) assume e in { (a + c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a ++ A then ex c being Element of COMPLEX st ( e = a + c & c in A ) ; hence e in a ++ A by Th141; ::_thesis: verum end; theorem Th143: :: MEMBER_1:143 for A being complex-membered set for a being complex number for e being set st e in a ++ A holds ex c being Element of COMPLEX st ( e = a + c & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in a ++ A holds ex c being Element of COMPLEX st ( e = a + c & c in A ) let e be set ; ::_thesis: ( e in a ++ A implies ex c being Element of COMPLEX st ( e = a + c & c in A ) ) a ++ A = { (a + c) where c is Element of COMPLEX : c in A } by Th142; hence ( e in a ++ A implies ex c being Element of COMPLEX st ( e = a + c & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clustera ++ A -> empty ; coherence a ++ A is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clustera ++ A -> non empty ; coherence not a ++ A is empty ; end; registration let A be complex-membered set ; let a be complex number ; clustera ++ A -> complex-membered ; coherence a ++ A is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clustera ++ A -> real-membered ; coherence a ++ A is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clustera ++ A -> rational-membered ; coherence a ++ A is rational-membered ; end; registration let A be integer-membered set ; let a be integer number ; clustera ++ A -> integer-membered ; coherence a ++ A is integer-membered ; end; registration let A be natural-membered set ; let a be Nat; clustera ++ A -> natural-membered ; coherence a ++ A is natural-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifya ++ A with f ++ F when A = F, a = f; compatibility ( A = F & a = f implies a ++ A = f ++ F ) ; end; theorem Th144: :: MEMBER_1:144 for A, B being complex-membered set for a being complex number holds ( A c= B iff a ++ A c= a ++ B ) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds ( A c= B iff a ++ A c= a ++ B ) let a be complex number ; ::_thesis: ( A c= B iff a ++ A c= a ++ B ) thus ( A c= B implies a ++ A c= a ++ B ) by Th47; ::_thesis: ( a ++ A c= a ++ B implies A c= B ) assume A1: a ++ A c= a ++ B ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then a + z in a ++ A by Th141; then ex c being Element of COMPLEX st ( a + z = a + c & c in B ) by A1, Th143; hence z in B ; ::_thesis: verum end; theorem :: MEMBER_1:145 for A, B being complex-membered set for a being complex number st a ++ A = a ++ B holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a ++ A = a ++ B holds A = B let a be complex number ; ::_thesis: ( a ++ A = a ++ B implies A = B ) assume a ++ A = a ++ B ; ::_thesis: A = B then ( A c= B & B c= A ) by Th144; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:146 for A being complex-membered set holds 0 ++ A = A proof let A be complex-membered set ; ::_thesis: 0 ++ A = A let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in 0 ++ A or a in A ) & ( not a in A or a in 0 ++ A ) ) hereby ::_thesis: ( not a in A or a in 0 ++ A ) assume a in 0 ++ A ; ::_thesis: a in A then consider c1, c2 being Element of COMPLEX such that A1: a = c1 + c2 and A2: c1 in {0} and A3: c2 in A ; c1 = 0 by A2, TARSKI:def_1; hence a in A by A1, A3; ::_thesis: verum end; assume a in A ; ::_thesis: a in 0 ++ A then 0 + a in { (0 + c) where c is Element of COMPLEX : c in A } ; hence a in 0 ++ A by Th142; ::_thesis: verum end; theorem :: MEMBER_1:147 for A being complex-membered set for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A) let a, b be complex number ; ::_thesis: (a + b) ++ A = a ++ (b ++ A) thus (a + b) ++ A = ({a} ++ {b}) ++ A by Th51 .= a ++ (b ++ A) by Th50 ; ::_thesis: verum end; theorem :: MEMBER_1:148 for A, B being complex-membered set for a being complex number holds a ++ (A ++ B) = (a ++ A) ++ B by Th50; theorem Th149: :: MEMBER_1:149 for A, B being complex-membered set for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B) let a be complex number ; ::_thesis: a ++ (A /\ B) = (a ++ A) /\ (a ++ B) A1: (a ++ A) /\ (a ++ B) c= a ++ (A /\ B) proof let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ++ A) /\ (a ++ B) or z in a ++ (A /\ B) ) assume A2: z in (a ++ A) /\ (a ++ B) ; ::_thesis: z in a ++ (A /\ B) then z in a ++ A by XBOOLE_0:def_4; then consider c being Element of COMPLEX such that A3: z = a + c and A4: c in A by Th143; z in a ++ B by A2, XBOOLE_0:def_4; then ex c1 being Element of COMPLEX st ( z = a + c1 & c1 in B ) by Th143; then c in A /\ B by A3, A4, XBOOLE_0:def_4; hence z in a ++ (A /\ B) by A3, Th141; ::_thesis: verum end; a ++ (A /\ B) c= (a ++ A) /\ (a ++ B) by Th49; hence a ++ (A /\ B) = (a ++ A) /\ (a ++ B) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th150: :: MEMBER_1:150 for A, B being complex-membered set for a being complex number holds a ++ (A \ B) = (a ++ A) \ (a ++ B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A \ B) = (a ++ A) \ (a ++ B) let a be complex number ; ::_thesis: a ++ (A \ B) = (a ++ A) \ (a ++ B) let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in a ++ (A \ B) or z in (a ++ A) \ (a ++ B) ) & ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) ) ) hereby ::_thesis: ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) ) assume z in a ++ (A \ B) ; ::_thesis: z in (a ++ A) \ (a ++ B) then consider c being Element of COMPLEX such that A1: z = a + c and A2: c in A \ B by Th143; A3: now__::_thesis:_not_a_+_c_in_a_++_B assume a + c in a ++ B ; ::_thesis: contradiction then ex c1 being Element of COMPLEX st ( a + c = a + c1 & c1 in B ) by Th143; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; a + c in a ++ A by A2, Th141; hence z in (a ++ A) \ (a ++ B) by A1, A3, XBOOLE_0:def_5; ::_thesis: verum end; assume A4: z in (a ++ A) \ (a ++ B) ; ::_thesis: z in a ++ (A \ B) then consider c being Element of COMPLEX such that A5: z = a + c and A6: c in A by Th143; now__::_thesis:_c_in_A_\_B assume not c in A \ B ; ::_thesis: contradiction then c in B by A6, XBOOLE_0:def_5; then a + c in a ++ B by Th141; hence contradiction by A4, A5, XBOOLE_0:def_5; ::_thesis: verum end; hence z in a ++ (A \ B) by A5, Th141; ::_thesis: verum end; theorem Th151: :: MEMBER_1:151 for A, B being complex-membered set for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B) let a be complex number ; ::_thesis: a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B) thus a ++ (A \+\ B) = (a ++ (A \ B)) \/ (a ++ (B \ A)) by Th48 .= ((a ++ A) \ (a ++ B)) \/ (a ++ (B \ A)) by Th150 .= (a ++ A) \+\ (a ++ B) by Th150 ; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcf -- F -> set equals :: MEMBER_1:def 15 {f} -- F; coherence {f} -- F is set ; end; :: deftheorem defines -- MEMBER_1:def_15_:_ for F being ext-real-membered set for f being ext-real number holds f -- F = {f} -- F; theorem Th152: :: MEMBER_1:152 for G being ext-real-membered set for g, f being ext-real number st g in G holds f - g in f -- G proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds f - g in f -- G let g, f be ext-real number ; ::_thesis: ( g in G implies f - g in f -- G ) f in {f} by TARSKI:def_1; hence ( g in G implies f - g in f -- G ) by Th55; ::_thesis: verum end; theorem Th153: :: MEMBER_1:153 for F being ext-real-membered set for f being ext-real number holds f -- F = { (f - w) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f -- F = { (f - w) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: f -- F = { (f - w) where w is Element of ExtREAL : w in F } thus f -- F c= { (f - w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f - w) where w is Element of ExtREAL : w in F } c= f -- F proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f -- F or e in { (f - w) where w is Element of ExtREAL : w in F } ) assume e in f -- F ; ::_thesis: e in { (f - w) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 + w2 and A2: ( w1 in {f} & w2 in -- F ) ; A3: w1 - (- w2) = w1 + w2 ; ( - w2 in F & w1 = f ) by A2, Th2, TARSKI:def_1; hence e in { (f - w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f - w) where w is Element of ExtREAL : w in F } or e in f -- F ) assume e in { (f - w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f -- F then ex w being Element of ExtREAL st ( e = f - w & w in F ) ; hence e in f -- F by Th152; ::_thesis: verum end; theorem Th154: :: MEMBER_1:154 for F being ext-real-membered set for f being ext-real number for e being set st e in f -- F holds ex w being Element of ExtREAL st ( e = f - w & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in f -- F holds ex w being Element of ExtREAL st ( e = f - w & w in F ) let e be set ; ::_thesis: ( e in f -- F implies ex w being Element of ExtREAL st ( e = f - w & w in F ) ) f -- F = { (f - w) where w is Element of ExtREAL : w in F } by Th153; hence ( e in f -- F implies ex w being Element of ExtREAL st ( e = f - w & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterf -- F -> empty ; coherence f -- F is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterf -- F -> non empty ; coherence not f -- F is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterf -- F -> ext-real-membered ; coherence f -- F is ext-real-membered ; end; theorem Th155: :: MEMBER_1:155 for F, G being ext-real-membered set for r being real number st r -- F c= r -- G holds F c= G proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r -- F c= r -- G holds F c= G let r be real number ; ::_thesis: ( r -- F c= r -- G implies F c= G ) assume A1: r -- F c= r -- G ; ::_thesis: F c= G let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F or i in G ) assume i in F ; ::_thesis: i in G then r - i in r -- F by Th152; then ex w being Element of ExtREAL st ( r - i = r - w & w in G ) by A1, Th154; hence i in G by XXREAL_3:12; ::_thesis: verum end; theorem :: MEMBER_1:156 for F, G being ext-real-membered set for r being real number st r -- F = r -- G holds F = G proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r -- F = r -- G holds F = G let r be real number ; ::_thesis: ( r -- F = r -- G implies F = G ) assume r -- F = r -- G ; ::_thesis: F = G then ( F c= G & G c= F ) by Th155; hence F = G by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th157: :: MEMBER_1:157 for F, G being ext-real-membered set for r being real number holds r -- (F /\ G) = (r -- F) /\ (r -- G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F /\ G) = (r -- F) /\ (r -- G) let r be real number ; ::_thesis: r -- (F /\ G) = (r -- F) /\ (r -- G) thus r -- (F /\ G) = r ++ ((-- F) /\ (-- G)) by Th6 .= (r ++ (-- F)) /\ (r ++ (-- G)) by Th137 .= (r -- F) /\ (r -- G) ; ::_thesis: verum end; theorem Th158: :: MEMBER_1:158 for F, G being ext-real-membered set for r being real number holds r -- (F \ G) = (r -- F) \ (r -- G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F \ G) = (r -- F) \ (r -- G) let r be real number ; ::_thesis: r -- (F \ G) = (r -- F) \ (r -- G) thus r -- (F \ G) = r ++ ((-- F) \ (-- G)) by Th7 .= (r ++ (-- F)) \ (r ++ (-- G)) by Th139 .= (r -- F) \ (r -- G) ; ::_thesis: verum end; theorem Th159: :: MEMBER_1:159 for F, G being ext-real-membered set for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G) let r be real number ; ::_thesis: r -- (F \+\ G) = (r -- F) \+\ (r -- G) thus r -- (F \+\ G) = r ++ ((-- F) \+\ (-- G)) by Th8 .= (r ++ (-- F)) \+\ (r ++ (-- G)) by Th140 .= (r -- F) \+\ (r -- G) ; ::_thesis: verum end; definition let A be complex-membered set ; let a be complex number ; funca -- A -> set equals :: MEMBER_1:def 16 {a} -- A; coherence {a} -- A is set ; end; :: deftheorem defines -- MEMBER_1:def_16_:_ for A being complex-membered set for a being complex number holds a -- A = {a} -- A; theorem Th160: :: MEMBER_1:160 for A being complex-membered set for b, a being complex number st b in A holds a - b in a -- A proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds a - b in a -- A let b, a be complex number ; ::_thesis: ( b in A implies a - b in a -- A ) a in {a} by TARSKI:def_1; hence ( b in A implies a - b in a -- A ) by Th66; ::_thesis: verum end; theorem Th161: :: MEMBER_1:161 for A being complex-membered set for a being complex number holds a -- A = { (a - c) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds a -- A = { (a - c) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: a -- A = { (a - c) where c is Element of COMPLEX : c in A } A1: a -- A = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in {a} & c2 in A ) } by Th65; thus a -- A c= { (a - c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a - c) where c is Element of COMPLEX : c in A } c= a -- A proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a -- A or e in { (a - c) where c is Element of COMPLEX : c in A } ) assume e in a -- A ; ::_thesis: e in { (a - c) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A2: e = c1 - c2 and A3: c1 in {a} and A4: c2 in A by A1; c1 = a by A3, TARSKI:def_1; hence e in { (a - c) where c is Element of COMPLEX : c in A } by A2, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a - c) where c is Element of COMPLEX : c in A } or e in a -- A ) assume e in { (a - c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a -- A then ex c being Element of COMPLEX st ( e = a - c & c in A ) ; hence e in a -- A by Th160; ::_thesis: verum end; theorem Th162: :: MEMBER_1:162 for A being complex-membered set for a being complex number for e being set st e in a -- A holds ex c being Element of COMPLEX st ( e = a - c & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in a -- A holds ex c being Element of COMPLEX st ( e = a - c & c in A ) let e be set ; ::_thesis: ( e in a -- A implies ex c being Element of COMPLEX st ( e = a - c & c in A ) ) a -- A = { (a - c) where c is Element of COMPLEX : c in A } by Th161; hence ( e in a -- A implies ex c being Element of COMPLEX st ( e = a - c & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clustera -- A -> empty ; coherence a -- A is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clustera -- A -> non empty ; coherence not a -- A is empty ; end; registration let A be complex-membered set ; let a be complex number ; clustera -- A -> complex-membered ; coherence a -- A is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clustera -- A -> real-membered ; coherence a -- A is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clustera -- A -> rational-membered ; coherence a -- A is rational-membered ; end; registration let A be integer-membered set ; let a be integer number ; clustera -- A -> integer-membered ; coherence a -- A is integer-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifya -- A with f -- F when A = F, a = f; compatibility ( A = F & a = f implies a -- A = f -- F ) ; end; theorem Th163: :: MEMBER_1:163 for A, B being complex-membered set for a being complex number holds ( A c= B iff a -- A c= a -- B ) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds ( A c= B iff a -- A c= a -- B ) let a be complex number ; ::_thesis: ( A c= B iff a -- A c= a -- B ) thus ( A c= B implies a -- A c= a -- B ) by Th67; ::_thesis: ( a -- A c= a -- B implies A c= B ) assume A1: a -- A c= a -- B ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then a - z in a -- A by Th160; then ex c being Element of COMPLEX st ( a - z = a - c & c in B ) by A1, Th162; hence z in B ; ::_thesis: verum end; theorem :: MEMBER_1:164 for A, B being complex-membered set for a being complex number st a -- A = a -- B holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a -- A = a -- B holds A = B let a be complex number ; ::_thesis: ( a -- A = a -- B implies A = B ) assume a -- A = a -- B ; ::_thesis: A = B then ( A c= B & B c= A ) by Th163; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th165: :: MEMBER_1:165 for A, B being complex-membered set for a being complex number holds a -- (A /\ B) = (a -- A) /\ (a -- B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A /\ B) = (a -- A) /\ (a -- B) let a be complex number ; ::_thesis: a -- (A /\ B) = (a -- A) /\ (a -- B) thus a -- (A /\ B) = a ++ ((-- A) /\ (-- B)) by Th16 .= (a ++ (-- A)) /\ (a ++ (-- B)) by Th149 .= (a -- A) /\ (a -- B) ; ::_thesis: verum end; theorem Th166: :: MEMBER_1:166 for A, B being complex-membered set for a being complex number holds a -- (A \ B) = (a -- A) \ (a -- B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A \ B) = (a -- A) \ (a -- B) let a be complex number ; ::_thesis: a -- (A \ B) = (a -- A) \ (a -- B) thus a -- (A \ B) = a ++ ((-- A) \ (-- B)) by Th17 .= (a ++ (-- A)) \ (a ++ (-- B)) by Th150 .= (a -- A) \ (a -- B) ; ::_thesis: verum end; theorem Th167: :: MEMBER_1:167 for A, B being complex-membered set for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B) let a be complex number ; ::_thesis: a -- (A \+\ B) = (a -- A) \+\ (a -- B) thus a -- (A \+\ B) = a ++ ((-- A) \+\ (-- B)) by Th18 .= (a ++ (-- A)) \+\ (a ++ (-- B)) by Th151 .= (a -- A) \+\ (a -- B) ; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcF -- f -> set equals :: MEMBER_1:def 17 F -- {f}; coherence F -- {f} is set ; end; :: deftheorem defines -- MEMBER_1:def_17_:_ for F being ext-real-membered set for f being ext-real number holds F -- f = F -- {f}; theorem Th168: :: MEMBER_1:168 for G being ext-real-membered set for g, f being ext-real number st g in G holds g - f in G -- f proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds g - f in G -- f let g, f be ext-real number ; ::_thesis: ( g in G implies g - f in G -- f ) f in {f} by TARSKI:def_1; hence ( g in G implies g - f in G -- f ) by Th55; ::_thesis: verum end; theorem Th169: :: MEMBER_1:169 for F being ext-real-membered set for f being ext-real number holds F -- f = { (w - f) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds F -- f = { (w - f) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: F -- f = { (w - f) where w is Element of ExtREAL : w in F } thus F -- f c= { (w - f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (w - f) where w is Element of ExtREAL : w in F } c= F -- f proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F -- f or e in { (w - f) where w is Element of ExtREAL : w in F } ) assume e in F -- f ; ::_thesis: e in { (w - f) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: ( e = w1 + w2 & w1 in F ) and A2: w2 in -- {f} ; - w2 in {f} by A2, Th2; then ( w1 - (- w2) = w1 + w2 & - w2 = f ) by TARSKI:def_1; hence e in { (w - f) where w is Element of ExtREAL : w in F } by A1; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w - f) where w is Element of ExtREAL : w in F } or e in F -- f ) assume e in { (w - f) where w is Element of ExtREAL : w in F } ; ::_thesis: e in F -- f then ex w being Element of ExtREAL st ( e = w - f & w in F ) ; hence e in F -- f by Th168; ::_thesis: verum end; theorem :: MEMBER_1:170 for F being ext-real-membered set for f being ext-real number for e being set st e in F -- f holds ex w being Element of ExtREAL st ( e = w - f & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in F -- f holds ex w being Element of ExtREAL st ( e = w - f & w in F ) let e be set ; ::_thesis: ( e in F -- f implies ex w being Element of ExtREAL st ( e = w - f & w in F ) ) F -- f = { (w - f) where w is Element of ExtREAL : w in F } by Th169; hence ( e in F -- f implies ex w being Element of ExtREAL st ( e = w - f & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterF -- f -> empty ; coherence F -- f is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterF -- f -> non empty ; coherence not F -- f is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterF -- f -> ext-real-membered ; coherence F -- f is ext-real-membered ; end; theorem :: MEMBER_1:171 for F being ext-real-membered set for f being ext-real number holds F -- f = -- (f -- F) by Th60; theorem :: MEMBER_1:172 for F being ext-real-membered set for f being ext-real number holds f -- F = -- (F -- f) by Th60; theorem :: MEMBER_1:173 for F, G being ext-real-membered set for r being real number holds (F /\ G) -- r = (F -- r) /\ (G -- r) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F /\ G) -- r = (F -- r) /\ (G -- r) let r be real number ; ::_thesis: (F /\ G) -- r = (F -- r) /\ (G -- r) thus (F /\ G) -- r = -- (r -- (F /\ G)) by Th60 .= -- ((r -- F) /\ (r -- G)) by Th157 .= (-- (r -- F)) /\ (-- (r -- G)) by Th6 .= (-- (r -- F)) /\ (G -- r) by Th60 .= (F -- r) /\ (G -- r) by Th60 ; ::_thesis: verum end; theorem :: MEMBER_1:174 for F, G being ext-real-membered set for r being real number holds (F \ G) -- r = (F -- r) \ (G -- r) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F \ G) -- r = (F -- r) \ (G -- r) let r be real number ; ::_thesis: (F \ G) -- r = (F -- r) \ (G -- r) thus (F \ G) -- r = -- (r -- (F \ G)) by Th60 .= -- ((r -- F) \ (r -- G)) by Th158 .= (-- (r -- F)) \ (-- (r -- G)) by Th7 .= (-- (r -- F)) \ (G -- r) by Th60 .= (F -- r) \ (G -- r) by Th60 ; ::_thesis: verum end; theorem :: MEMBER_1:175 for F, G being ext-real-membered set for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r) let r be real number ; ::_thesis: (F \+\ G) -- r = (F -- r) \+\ (G -- r) thus (F \+\ G) -- r = -- (r -- (F \+\ G)) by Th60 .= -- ((r -- F) \+\ (r -- G)) by Th159 .= (-- (r -- F)) \+\ (-- (r -- G)) by Th8 .= (-- (r -- F)) \+\ (G -- r) by Th60 .= (F -- r) \+\ (G -- r) by Th60 ; ::_thesis: verum end; definition let A be complex-membered set ; let a be complex number ; funcA -- a -> set equals :: MEMBER_1:def 18 A -- {a}; coherence A -- {a} is set ; end; :: deftheorem defines -- MEMBER_1:def_18_:_ for A being complex-membered set for a being complex number holds A -- a = A -- {a}; theorem Th176: :: MEMBER_1:176 for A being complex-membered set for b, a being complex number st b in A holds b - a in A -- a proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds b - a in A -- a let b, a be complex number ; ::_thesis: ( b in A implies b - a in A -- a ) a in {a} by TARSKI:def_1; hence ( b in A implies b - a in A -- a ) by Th66; ::_thesis: verum end; theorem Th177: :: MEMBER_1:177 for A being complex-membered set for a being complex number holds A -- a = { (c - a) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds A -- a = { (c - a) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: A -- a = { (c - a) where c is Element of COMPLEX : c in A } A1: A -- a = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in {a} ) } by Th65; thus A -- a c= { (c - a) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c - a) where c is Element of COMPLEX : c in A } c= A -- a proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A -- a or e in { (c - a) where c is Element of COMPLEX : c in A } ) assume e in A -- a ; ::_thesis: e in { (c - a) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A2: ( e = c1 - c2 & c1 in A ) and A3: c2 in {a} by A1; c2 = a by A3, TARSKI:def_1; hence e in { (c - a) where c is Element of COMPLEX : c in A } by A2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c - a) where c is Element of COMPLEX : c in A } or e in A -- a ) assume e in { (c - a) where c is Element of COMPLEX : c in A } ; ::_thesis: e in A -- a then ex c being Element of COMPLEX st ( e = c - a & c in A ) ; hence e in A -- a by Th176; ::_thesis: verum end; theorem Th178: :: MEMBER_1:178 for A being complex-membered set for a being complex number for e being set st e in A -- a holds ex c being Element of COMPLEX st ( e = c - a & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in A -- a holds ex c being Element of COMPLEX st ( e = c - a & c in A ) let e be set ; ::_thesis: ( e in A -- a implies ex c being Element of COMPLEX st ( e = c - a & c in A ) ) A -- a = { (c - a) where c is Element of COMPLEX : c in A } by Th177; hence ( e in A -- a implies ex c being Element of COMPLEX st ( e = c - a & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clusterA -- a -> empty ; coherence A -- a is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clusterA -- a -> non empty ; coherence not A -- a is empty ; end; registration let A be complex-membered set ; let a be complex number ; clusterA -- a -> complex-membered ; coherence A -- a is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clusterA -- a -> real-membered ; coherence A -- a is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clusterA -- a -> rational-membered ; coherence A -- a is rational-membered ; end; registration let A be integer-membered set ; let a be integer number ; clusterA -- a -> integer-membered ; coherence A -- a is integer-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifyA -- a with F -- f when A = F, a = f; compatibility ( A = F & a = f implies A -- a = F -- f ) ; end; theorem Th179: :: MEMBER_1:179 for A, B being complex-membered set for a being complex number holds ( A c= B iff A -- a c= B -- a ) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds ( A c= B iff A -- a c= B -- a ) let a be complex number ; ::_thesis: ( A c= B iff A -- a c= B -- a ) thus ( A c= B implies A -- a c= B -- a ) by Th67; ::_thesis: ( A -- a c= B -- a implies A c= B ) assume A1: A -- a c= B -- a ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then z - a in A -- a by Th176; then ex c being Element of COMPLEX st ( z - a = c - a & c in B ) by A1, Th178; hence z in B ; ::_thesis: verum end; theorem :: MEMBER_1:180 for A, B being complex-membered set for a being complex number st A -- a = B -- a holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st A -- a = B -- a holds A = B let a be complex number ; ::_thesis: ( A -- a = B -- a implies A = B ) assume A -- a = B -- a ; ::_thesis: A = B then ( A c= B & B c= A ) by Th179; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:181 for A being complex-membered set for a being complex number holds A -- a = -- (a -- A) by Th71; theorem :: MEMBER_1:182 for A being complex-membered set for a being complex number holds a -- A = -- (A -- a) by Th71; theorem :: MEMBER_1:183 for A, B being complex-membered set for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a) let a be complex number ; ::_thesis: (A /\ B) -- a = (A -- a) /\ (B -- a) thus (A /\ B) -- a = -- (a -- (A /\ B)) by Th71 .= -- ((a -- A) /\ (a -- B)) by Th165 .= (-- (a -- A)) /\ (-- (a -- B)) by Th16 .= (-- (a -- A)) /\ (B -- a) by Th71 .= (A -- a) /\ (B -- a) by Th71 ; ::_thesis: verum end; theorem :: MEMBER_1:184 for A, B being complex-membered set for a being complex number holds (A \ B) -- a = (A -- a) \ (B -- a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A \ B) -- a = (A -- a) \ (B -- a) let a be complex number ; ::_thesis: (A \ B) -- a = (A -- a) \ (B -- a) thus (A \ B) -- a = -- (a -- (A \ B)) by Th71 .= -- ((a -- A) \ (a -- B)) by Th166 .= (-- (a -- A)) \ (-- (a -- B)) by Th17 .= (-- (a -- A)) \ (B -- a) by Th71 .= (A -- a) \ (B -- a) by Th71 ; ::_thesis: verum end; theorem :: MEMBER_1:185 for A, B being complex-membered set for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a) let a be complex number ; ::_thesis: (A \+\ B) -- a = (A -- a) \+\ (B -- a) thus (A \+\ B) -- a = -- (a -- (A \+\ B)) by Th71 .= -- ((a -- A) \+\ (a -- B)) by Th167 .= (-- (a -- A)) \+\ (-- (a -- B)) by Th18 .= (-- (a -- A)) \+\ (B -- a) by Th71 .= (A -- a) \+\ (B -- a) by Th71 ; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcf ** F -> set equals :: MEMBER_1:def 19 {f} ** F; coherence {f} ** F is set ; end; :: deftheorem defines ** MEMBER_1:def_19_:_ for F being ext-real-membered set for f being ext-real number holds f ** F = {f} ** F; theorem Th186: :: MEMBER_1:186 for G being ext-real-membered set for g, f being ext-real number st g in G holds f * g in f ** G proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds f * g in f ** G let g, f be ext-real number ; ::_thesis: ( g in G implies f * g in f ** G ) f in {f} by TARSKI:def_1; hence ( g in G implies f * g in f ** G ) by Th79; ::_thesis: verum end; theorem Th187: :: MEMBER_1:187 for F being ext-real-membered set for f being ext-real number holds f ** F = { (f * w) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f ** F = { (f * w) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: f ** F = { (f * w) where w is Element of ExtREAL : w in F } thus f ** F c= { (f * w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f * w) where w is Element of ExtREAL : w in F } c= f ** F proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f ** F or e in { (f * w) where w is Element of ExtREAL : w in F } ) assume e in f ** F ; ::_thesis: e in { (f * w) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 * w2 and A2: w1 in {f} and A3: w2 in F ; w1 = f by A2, TARSKI:def_1; hence e in { (f * w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f * w) where w is Element of ExtREAL : w in F } or e in f ** F ) assume e in { (f * w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f ** F then ex w being Element of ExtREAL st ( e = f * w & w in F ) ; hence e in f ** F by Th186; ::_thesis: verum end; theorem Th188: :: MEMBER_1:188 for F being ext-real-membered set for f being ext-real number for e being set st e in f ** F holds ex w being Element of ExtREAL st ( e = f * w & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in f ** F holds ex w being Element of ExtREAL st ( e = f * w & w in F ) let e be set ; ::_thesis: ( e in f ** F implies ex w being Element of ExtREAL st ( e = f * w & w in F ) ) f ** F = { (f * w) where w is Element of ExtREAL : w in F } by Th187; hence ( e in f ** F implies ex w being Element of ExtREAL st ( e = f * w & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterf ** F -> empty ; coherence f ** F is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterf ** F -> non empty ; coherence not f ** F is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterf ** F -> ext-real-membered ; coherence f ** F is ext-real-membered ; end; theorem :: MEMBER_1:189 for F, G being ext-real-membered set for r being real number st r <> 0 holds r ** (F /\ G) = (r ** F) /\ (r ** G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds r ** (F /\ G) = (r ** F) /\ (r ** G) let r be real number ; ::_thesis: ( r <> 0 implies r ** (F /\ G) = (r ** F) /\ (r ** G) ) assume A1: r <> 0 ; ::_thesis: r ** (F /\ G) = (r ** F) /\ (r ** G) A2: (r ** F) /\ (r ** G) c= r ** (F /\ G) proof let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in (r ** F) /\ (r ** G) or j in r ** (F /\ G) ) assume A3: j in (r ** F) /\ (r ** G) ; ::_thesis: j in r ** (F /\ G) then j in r ** F by XBOOLE_0:def_4; then consider w being Element of ExtREAL such that A4: j = r * w and A5: w in F by Th188; j in r ** G by A3, XBOOLE_0:def_4; then consider w1 being Element of ExtREAL such that A6: j = r * w1 and A7: w1 in G by Th188; w = w1 by A1, A4, A6, XXREAL_3:68; then w in F /\ G by A5, A7, XBOOLE_0:def_4; hence j in r ** (F /\ G) by A4, Th186; ::_thesis: verum end; r ** (F /\ G) c= (r ** F) /\ (r ** G) by Th83; hence r ** (F /\ G) = (r ** F) /\ (r ** G) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th190: :: MEMBER_1:190 for F, G being ext-real-membered set for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G) proof let F, G be ext-real-membered set ; ::_thesis: for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G) let f be ext-real number ; ::_thesis: (f ** F) \ (f ** G) c= f ** (F \ G) let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (f ** F) \ (f ** G) or i in f ** (F \ G) ) assume A1: i in (f ** F) \ (f ** G) ; ::_thesis: i in f ** (F \ G) then consider w being Element of ExtREAL such that A2: i = f * w and A3: w in F by Th188; now__::_thesis:_w_in_F_\_G assume not w in F \ G ; ::_thesis: contradiction then w in G by A3, XBOOLE_0:def_5; then f * w in f ** G by Th186; hence contradiction by A1, A2, XBOOLE_0:def_5; ::_thesis: verum end; hence i in f ** (F \ G) by A2, Th186; ::_thesis: verum end; theorem Th191: :: MEMBER_1:191 for F, G being ext-real-membered set for r being real number st r <> 0 holds r ** (F \ G) = (r ** F) \ (r ** G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds r ** (F \ G) = (r ** F) \ (r ** G) let r be real number ; ::_thesis: ( r <> 0 implies r ** (F \ G) = (r ** F) \ (r ** G) ) assume A1: r <> 0 ; ::_thesis: r ** (F \ G) = (r ** F) \ (r ** G) A2: r ** (F \ G) c= (r ** F) \ (r ** G) proof let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in r ** (F \ G) or i in (r ** F) \ (r ** G) ) assume i in r ** (F \ G) ; ::_thesis: i in (r ** F) \ (r ** G) then consider w being Element of ExtREAL such that A3: i = r * w and A4: w in F \ G by Th188; A5: now__::_thesis:_not_r_*_w_in_r_**_G assume r * w in r ** G ; ::_thesis: contradiction then consider w1 being Element of ExtREAL such that A6: r * w = r * w1 and A7: w1 in G by Th188; w = w1 by A1, A6, XXREAL_3:68; hence contradiction by A4, A7, XBOOLE_0:def_5; ::_thesis: verum end; r * w in r ** F by A4, Th186; hence i in (r ** F) \ (r ** G) by A3, A5, XBOOLE_0:def_5; ::_thesis: verum end; (r ** F) \ (r ** G) c= r ** (F \ G) by Th190; hence r ** (F \ G) = (r ** F) \ (r ** G) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:192 for F, G being ext-real-membered set for r being real number st r <> 0 holds r ** (F \+\ G) = (r ** F) \+\ (r ** G) proof let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds r ** (F \+\ G) = (r ** F) \+\ (r ** G) let r be real number ; ::_thesis: ( r <> 0 implies r ** (F \+\ G) = (r ** F) \+\ (r ** G) ) assume A1: r <> 0 ; ::_thesis: r ** (F \+\ G) = (r ** F) \+\ (r ** G) thus r ** (F \+\ G) = (r ** (F \ G)) \/ (r ** (G \ F)) by Th82 .= ((r ** F) \ (r ** G)) \/ (r ** (G \ F)) by A1, Th191 .= (r ** F) \+\ (r ** G) by A1, Th191 ; ::_thesis: verum end; definition let A be complex-membered set ; let a be complex number ; funca ** A -> set equals :: MEMBER_1:def 20 {a} ** A; coherence {a} ** A is set ; end; :: deftheorem defines ** MEMBER_1:def_20_:_ for A being complex-membered set for a being complex number holds a ** A = {a} ** A; theorem Th193: :: MEMBER_1:193 for A being complex-membered set for b, a being complex number st b in A holds a * b in a ** A proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds a * b in a ** A let b, a be complex number ; ::_thesis: ( b in A implies a * b in a ** A ) a in {a} by TARSKI:def_1; hence ( b in A implies a * b in a ** A ) by Th89; ::_thesis: verum end; theorem Th194: :: MEMBER_1:194 for A being complex-membered set for a being complex number holds a ** A = { (a * c) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds a ** A = { (a * c) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: a ** A = { (a * c) where c is Element of COMPLEX : c in A } thus a ** A c= { (a * c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a * c) where c is Element of COMPLEX : c in A } c= a ** A proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a ** A or e in { (a * c) where c is Element of COMPLEX : c in A } ) assume e in a ** A ; ::_thesis: e in { (a * c) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A1: e = c1 * c2 and A2: c1 in {a} and A3: c2 in A ; c1 = a by A2, TARSKI:def_1; hence e in { (a * c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a * c) where c is Element of COMPLEX : c in A } or e in a ** A ) assume e in { (a * c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a ** A then ex c being Element of COMPLEX st ( e = a * c & c in A ) ; hence e in a ** A by Th193; ::_thesis: verum end; theorem Th195: :: MEMBER_1:195 for A being complex-membered set for a being complex number for e being set st e in a ** A holds ex c being Element of COMPLEX st ( e = a * c & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in a ** A holds ex c being Element of COMPLEX st ( e = a * c & c in A ) let e be set ; ::_thesis: ( e in a ** A implies ex c being Element of COMPLEX st ( e = a * c & c in A ) ) a ** A = { (a * c) where c is Element of COMPLEX : c in A } by Th194; hence ( e in a ** A implies ex c being Element of COMPLEX st ( e = a * c & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clustera ** A -> empty ; coherence a ** A is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clustera ** A -> non empty ; coherence not a ** A is empty ; end; registration let A be complex-membered set ; let a be complex number ; clustera ** A -> complex-membered ; coherence a ** A is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clustera ** A -> real-membered ; coherence a ** A is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clustera ** A -> rational-membered ; coherence a ** A is rational-membered ; end; registration let A be integer-membered set ; let a be integer number ; clustera ** A -> integer-membered ; coherence a ** A is integer-membered ; end; registration let A be natural-membered set ; let a be Nat; clustera ** A -> natural-membered ; coherence a ** A is natural-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifya ** A with f ** F when A = F, a = f; compatibility ( A = F & a = f implies a ** A = f ** F ) ; end; theorem Th196: :: MEMBER_1:196 for A, B being complex-membered set for a being complex number st a <> 0 & a ** A c= a ** B holds A c= B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a ** A c= a ** B holds A c= B let a be complex number ; ::_thesis: ( a <> 0 & a ** A c= a ** B implies A c= B ) assume that A1: a <> 0 and A2: a ** A c= a ** B ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then a * z in a ** A by Th193; then ex c being Element of COMPLEX st ( a * z = a * c & c in B ) by A2, Th195; hence z in B by A1, XCMPLX_1:5; ::_thesis: verum end; theorem :: MEMBER_1:197 for A, B being complex-membered set for a being complex number st a <> 0 & a ** A = a ** B holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a ** A = a ** B holds A = B let a be complex number ; ::_thesis: ( a <> 0 & a ** A = a ** B implies A = B ) assume ( a <> 0 & a ** A = a ** B ) ; ::_thesis: A = B then ( A c= B & B c= A ) by Th196; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th198: :: MEMBER_1:198 for A, B being complex-membered set for a being complex number st a <> 0 holds a ** (A /\ B) = (a ** A) /\ (a ** B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a ** (A /\ B) = (a ** A) /\ (a ** B) let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A /\ B) = (a ** A) /\ (a ** B) ) assume A1: a <> 0 ; ::_thesis: a ** (A /\ B) = (a ** A) /\ (a ** B) A2: (a ** A) /\ (a ** B) c= a ** (A /\ B) proof let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ** A) /\ (a ** B) or z in a ** (A /\ B) ) assume A3: z in (a ** A) /\ (a ** B) ; ::_thesis: z in a ** (A /\ B) then z in a ** A by XBOOLE_0:def_4; then consider c being Element of COMPLEX such that A4: z = a * c and A5: c in A by Th195; z in a ** B by A3, XBOOLE_0:def_4; then consider c1 being Element of COMPLEX such that A6: z = a * c1 and A7: c1 in B by Th195; c = c1 by A1, A4, A6, XCMPLX_1:5; then c in A /\ B by A5, A7, XBOOLE_0:def_4; hence z in a ** (A /\ B) by A4, Th193; ::_thesis: verum end; a ** (A /\ B) c= (a ** A) /\ (a ** B) by Th93; hence a ** (A /\ B) = (a ** A) /\ (a ** B) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th199: :: MEMBER_1:199 for A, B being complex-membered set for a being complex number st a <> 0 holds a ** (A \ B) = (a ** A) \ (a ** B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a ** (A \ B) = (a ** A) \ (a ** B) let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A \ B) = (a ** A) \ (a ** B) ) assume A1: a <> 0 ; ::_thesis: a ** (A \ B) = (a ** A) \ (a ** B) let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in a ** (A \ B) or z in (a ** A) \ (a ** B) ) & ( not z in (a ** A) \ (a ** B) or z in a ** (A \ B) ) ) hereby ::_thesis: ( not z in (a ** A) \ (a ** B) or z in a ** (A \ B) ) assume z in a ** (A \ B) ; ::_thesis: z in (a ** A) \ (a ** B) then consider c being Element of COMPLEX such that A2: z = a * c and A3: c in A \ B by Th195; A4: now__::_thesis:_not_a_*_c_in_a_**_B assume a * c in a ** B ; ::_thesis: contradiction then consider c1 being Element of COMPLEX such that A5: a * c = a * c1 and A6: c1 in B by Th195; c = c1 by A1, A5, XCMPLX_1:5; hence contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum end; a * c in a ** A by A3, Th193; hence z in (a ** A) \ (a ** B) by A2, A4, XBOOLE_0:def_5; ::_thesis: verum end; assume A7: z in (a ** A) \ (a ** B) ; ::_thesis: z in a ** (A \ B) then consider c being Element of COMPLEX such that A8: z = a * c and A9: c in A by Th195; now__::_thesis:_c_in_A_\_B assume not c in A \ B ; ::_thesis: contradiction then c in B by A9, XBOOLE_0:def_5; then a * c in a ** B by Th193; hence contradiction by A7, A8, XBOOLE_0:def_5; ::_thesis: verum end; hence z in a ** (A \ B) by A8, Th193; ::_thesis: verum end; theorem Th200: :: MEMBER_1:200 for A, B being complex-membered set for a being complex number st a <> 0 holds a ** (A \+\ B) = (a ** A) \+\ (a ** B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a ** (A \+\ B) = (a ** A) \+\ (a ** B) let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A \+\ B) = (a ** A) \+\ (a ** B) ) assume A1: a <> 0 ; ::_thesis: a ** (A \+\ B) = (a ** A) \+\ (a ** B) thus a ** (A \+\ B) = (a ** (A \ B)) \/ (a ** (B \ A)) by Th92 .= ((a ** A) \ (a ** B)) \/ (a ** (B \ A)) by A1, Th199 .= (a ** A) \+\ (a ** B) by A1, Th199 ; ::_thesis: verum end; theorem Th201: :: MEMBER_1:201 for A being complex-membered set holds 0 ** A c= {0} proof let A be complex-membered set ; ::_thesis: 0 ** A c= {0} let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in 0 ** A or a in {0} ) assume a in 0 ** A ; ::_thesis: a in {0} then consider c1, c2 being Element of COMPLEX such that A1: a = c1 * c2 and A2: c1 in {0} and c2 in A ; c1 = 0 by A2, TARSKI:def_1; hence a in {0} by A1, TARSKI:def_1; ::_thesis: verum end; theorem :: MEMBER_1:202 for A being complex-membered set st A <> {} holds 0 ** A = {0} proof let A be complex-membered set ; ::_thesis: ( A <> {} implies 0 ** A = {0} ) assume A1: A <> {} ; ::_thesis: 0 ** A = {0} A2: {0} c= 0 ** A proof set x = the Element of A; let a be Nat; :: according to MEMBERED:def_12 ::_thesis: ( not a in {0} or a in 0 ** A ) assume A3: a in {0} ; ::_thesis: a in 0 ** A the Element of A in COMPLEX by XCMPLX_0:def_2; then A4: 0 * the Element of A in { (0 * c) where c is Element of COMPLEX : c in A } by A1; 0 ** A = { (0 * c) where c is Element of COMPLEX : c in A } by Th194; hence a in 0 ** A by A3, A4, TARSKI:def_1; ::_thesis: verum end; 0 ** A c= {0} by Th201; hence 0 ** A = {0} by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:203 for A being complex-membered set holds 1 ** A = A proof let A be complex-membered set ; ::_thesis: 1 ** A = A let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in 1 ** A or a in A ) & ( not a in A or a in 1 ** A ) ) hereby ::_thesis: ( not a in A or a in 1 ** A ) assume a in 1 ** A ; ::_thesis: a in A then consider c1, c2 being Element of COMPLEX such that A1: a = c1 * c2 and A2: c1 in {1} and A3: c2 in A ; c1 = 1 by A2, TARSKI:def_1; hence a in A by A1, A3; ::_thesis: verum end; assume a in A ; ::_thesis: a in 1 ** A then 1 * a in { (1 * c) where c is Element of COMPLEX : c in A } ; hence a in 1 ** A by Th194; ::_thesis: verum end; theorem :: MEMBER_1:204 for A being complex-membered set for a, b being complex number holds (a * b) ** A = a ** (b ** A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a * b) ** A = a ** (b ** A) let a, b be complex number ; ::_thesis: (a * b) ** A = a ** (b ** A) thus (a * b) ** A = ({a} ** {b}) ** A by Th98 .= a ** (b ** A) by Th90 ; ::_thesis: verum end; theorem :: MEMBER_1:205 for A, B being complex-membered set for a being complex number holds a ** (A ** B) = (a ** A) ** B by Th90; theorem :: MEMBER_1:206 for A being complex-membered set for a, b being complex number holds (a + b) ** A c= (a ** A) ++ (b ** A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) ** A c= (a ** A) ++ (b ** A) let a, b be complex number ; ::_thesis: (a + b) ** A c= (a ** A) ++ (b ** A) {a} ++ {b} = {(a + b)} by Th51; hence (a + b) ** A c= (a ** A) ++ (b ** A) by Th95; ::_thesis: verum end; theorem :: MEMBER_1:207 for A being complex-membered set for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A) let a, b be complex number ; ::_thesis: (a - b) ** A c= (a ** A) -- (b ** A) {a} -- {b} = {(a - b)} by Th75; hence (a - b) ** A c= (a ** A) -- (b ** A) by Th96; ::_thesis: verum end; theorem Th208: :: MEMBER_1:208 for B, C being complex-membered set for a being complex number holds a ** (B ++ C) = (a ** B) ++ (a ** C) proof let B, C be complex-membered set ; ::_thesis: for a being complex number holds a ** (B ++ C) = (a ** B) ++ (a ** C) let a be complex number ; ::_thesis: a ** (B ++ C) = (a ** B) ++ (a ** C) A1: (a ** B) ++ (a ** C) c= a ** (B ++ C) proof let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ** B) ++ (a ** C) or z in a ** (B ++ C) ) assume z in (a ** B) ++ (a ** C) ; ::_thesis: z in a ** (B ++ C) then consider c, c1 being Element of COMPLEX such that A2: z = c + c1 and A3: c in a ** B and A4: c1 in a ** C ; consider c3 being Element of COMPLEX such that A5: c1 = a * c3 and A6: c3 in C by A4, Th195; consider c2 being Element of COMPLEX such that A7: c = a * c2 and A8: c2 in B by A3, Th195; A9: c2 + c3 in B ++ C by A8, A6; z = a * (c2 + c3) by A2, A7, A5; hence z in a ** (B ++ C) by A9, Th193; ::_thesis: verum end; a ** (B ++ C) c= (a ** B) ++ (a ** C) by Th95; hence a ** (B ++ C) = (a ** B) ++ (a ** C) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:209 for B, C being complex-membered set for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C) proof let B, C be complex-membered set ; ::_thesis: for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C) let a be complex number ; ::_thesis: a ** (B -- C) = (a ** B) -- (a ** C) thus a ** (B -- C) = (a ** B) ++ (a ** (-- C)) by Th208 .= (a ** B) -- (a ** C) by Th94 ; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcf /// F -> set equals :: MEMBER_1:def 21 {f} /// F; coherence {f} /// F is set ; end; :: deftheorem defines /// MEMBER_1:def_21_:_ for F being ext-real-membered set for f being ext-real number holds f /// F = {f} /// F; theorem Th210: :: MEMBER_1:210 for G being ext-real-membered set for g, f being ext-real number st g in G holds f / g in f /// G proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds f / g in f /// G let g, f be ext-real number ; ::_thesis: ( g in G implies f / g in f /// G ) f in {f} by TARSKI:def_1; hence ( g in G implies f / g in f /// G ) by Th102; ::_thesis: verum end; theorem Th211: :: MEMBER_1:211 for F being ext-real-membered set for f being ext-real number holds f /// F = { (f / w) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f /// F = { (f / w) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: f /// F = { (f / w) where w is Element of ExtREAL : w in F } thus f /// F c= { (f / w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f / w) where w is Element of ExtREAL : w in F } c= f /// F proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f /// F or e in { (f / w) where w is Element of ExtREAL : w in F } ) assume e in f /// F ; ::_thesis: e in { (f / w) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: e = w1 * w2 and A2: w1 in {f} and A3: w2 in F "" ; consider w3 being Element of ExtREAL such that A4: ( w2 = w3 " & w3 in F ) by A3; ( w1 * (w3 ") = w1 / w3 & w1 = f ) by A2, TARSKI:def_1; hence e in { (f / w) where w is Element of ExtREAL : w in F } by A1, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f / w) where w is Element of ExtREAL : w in F } or e in f /// F ) assume e in { (f / w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f /// F then ex w being Element of ExtREAL st ( e = f / w & w in F ) ; hence e in f /// F by Th210; ::_thesis: verum end; theorem :: MEMBER_1:212 for F being ext-real-membered set for f being ext-real number for e being set st e in f /// F holds ex w being Element of ExtREAL st ( e = f / w & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in f /// F holds ex w being Element of ExtREAL st ( e = f / w & w in F ) let e be set ; ::_thesis: ( e in f /// F implies ex w being Element of ExtREAL st ( e = f / w & w in F ) ) f /// F = { (f / w) where w is Element of ExtREAL : w in F } by Th211; hence ( e in f /// F implies ex w being Element of ExtREAL st ( e = f / w & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterf /// F -> empty ; coherence f /// F is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterf /// F -> non empty ; coherence not f /// F is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterf /// F -> ext-real-membered ; coherence f /// F is ext-real-membered ; end; definition let A be complex-membered set ; let a be complex number ; funca /// A -> set equals :: MEMBER_1:def 22 {a} /// A; coherence {a} /// A is set ; end; :: deftheorem defines /// MEMBER_1:def_22_:_ for A being complex-membered set for a being complex number holds a /// A = {a} /// A; theorem Th213: :: MEMBER_1:213 for A being complex-membered set for b, a being complex number st b in A holds a / b in a /// A proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds a / b in a /// A let b, a be complex number ; ::_thesis: ( b in A implies a / b in a /// A ) a in {a} by TARSKI:def_1; hence ( b in A implies a / b in a /// A ) by Th116; ::_thesis: verum end; theorem Th214: :: MEMBER_1:214 for A being complex-membered set for a being complex number holds a /// A = { (a / c) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds a /// A = { (a / c) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: a /// A = { (a / c) where c is Element of COMPLEX : c in A } thus a /// A c= { (a / c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a / c) where c is Element of COMPLEX : c in A } c= a /// A proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a /// A or e in { (a / c) where c is Element of COMPLEX : c in A } ) assume e in a /// A ; ::_thesis: e in { (a / c) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A1: e = c1 * c2 and A2: ( c1 in {a} & c2 in A "" ) ; A3: c1 * c2 = c1 / (c2 ") ; ( c2 " in A & c1 = a ) by A2, Th29, TARSKI:def_1; hence e in { (a / c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a / c) where c is Element of COMPLEX : c in A } or e in a /// A ) assume e in { (a / c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a /// A then ex c being Element of COMPLEX st ( e = a / c & c in A ) ; hence e in a /// A by Th213; ::_thesis: verum end; theorem Th215: :: MEMBER_1:215 for A being complex-membered set for a being complex number for e being set st e in a /// A holds ex c being Element of COMPLEX st ( e = a / c & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in a /// A holds ex c being Element of COMPLEX st ( e = a / c & c in A ) let e be set ; ::_thesis: ( e in a /// A implies ex c being Element of COMPLEX st ( e = a / c & c in A ) ) a /// A = { (a / c) where c is Element of COMPLEX : c in A } by Th214; hence ( e in a /// A implies ex c being Element of COMPLEX st ( e = a / c & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clustera /// A -> empty ; coherence a /// A is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clustera /// A -> non empty ; coherence not a /// A is empty ; end; registration let A be complex-membered set ; let a be complex number ; clustera /// A -> complex-membered ; coherence a /// A is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clustera /// A -> real-membered ; coherence a /// A is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clustera /// A -> rational-membered ; coherence a /// A is rational-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifya /// A with f /// F when A = F, a = f; compatibility ( A = F & a = f implies a /// A = f /// F ) ; end; theorem Th216: :: MEMBER_1:216 for A, B being complex-membered set for a being complex number st a <> 0 & a /// A c= a /// B holds A c= B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a /// A c= a /// B holds A c= B let a be complex number ; ::_thesis: ( a <> 0 & a /// A c= a /// B implies A c= B ) assume that A1: a <> 0 and A2: a /// A c= a /// B ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then a / z in a /// A by Th213; then consider c being Element of COMPLEX such that A3: a / z = a / c and A4: c in B by A2, Th215; z " = c " by A1, A3, XCMPLX_1:5; hence z in B by A4, XCMPLX_1:201; ::_thesis: verum end; theorem :: MEMBER_1:217 for A, B being complex-membered set for a being complex number st a <> 0 & a /// A = a /// B holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a /// A = a /// B holds A = B let a be complex number ; ::_thesis: ( a <> 0 & a /// A = a /// B implies A = B ) assume ( a <> 0 & a /// A = a /// B ) ; ::_thesis: A = B then ( A c= B & B c= A ) by Th216; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:218 for A, B being complex-membered set for a being complex number st a <> 0 holds a /// (A /\ B) = (a /// A) /\ (a /// B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a /// (A /\ B) = (a /// A) /\ (a /// B) let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A /\ B) = (a /// A) /\ (a /// B) ) assume A1: a <> 0 ; ::_thesis: a /// (A /\ B) = (a /// A) /\ (a /// B) thus a /// (A /\ B) = a ** ((A "") /\ (B "")) by Th33 .= (a ** (A "")) /\ (a ** (B "")) by A1, Th198 .= (a /// A) /\ (a /// B) ; ::_thesis: verum end; theorem :: MEMBER_1:219 for A, B being complex-membered set for a being complex number st a <> 0 holds a /// (A \ B) = (a /// A) \ (a /// B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a /// (A \ B) = (a /// A) \ (a /// B) let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A \ B) = (a /// A) \ (a /// B) ) assume A1: a <> 0 ; ::_thesis: a /// (A \ B) = (a /// A) \ (a /// B) thus a /// (A \ B) = a ** ((A "") \ (B "")) by Th34 .= (a ** (A "")) \ (a ** (B "")) by A1, Th199 .= (a /// A) \ (a /// B) ; ::_thesis: verum end; theorem :: MEMBER_1:220 for A, B being complex-membered set for a being complex number st a <> 0 holds a /// (A \+\ B) = (a /// A) \+\ (a /// B) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds a /// (A \+\ B) = (a /// A) \+\ (a /// B) let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A \+\ B) = (a /// A) \+\ (a /// B) ) assume A1: a <> 0 ; ::_thesis: a /// (A \+\ B) = (a /// A) \+\ (a /// B) thus a /// (A \+\ B) = a ** ((A "") \+\ (B "")) by Th35 .= (a ** (A "")) \+\ (a ** (B "")) by A1, Th200 .= (a /// A) \+\ (a /// B) ; ::_thesis: verum end; theorem :: MEMBER_1:221 for A being complex-membered set for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A) let a, b be complex number ; ::_thesis: (a + b) /// A c= (a /// A) ++ (b /// A) {a} ++ {b} = {(a + b)} by Th51; hence (a + b) /// A c= (a /// A) ++ (b /// A) by Th95; ::_thesis: verum end; theorem :: MEMBER_1:222 for A being complex-membered set for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A) proof let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A) let a, b be complex number ; ::_thesis: (a - b) /// A c= (a /// A) -- (b /// A) {a} -- {b} = {(a - b)} by Th75; hence (a - b) /// A c= (a /// A) -- (b /// A) by Th96; ::_thesis: verum end; definition let F be ext-real-membered set ; let f be ext-real number ; funcF /// f -> set equals :: MEMBER_1:def 23 F /// {f}; coherence F /// {f} is set ; end; :: deftheorem defines /// MEMBER_1:def_23_:_ for F being ext-real-membered set for f being ext-real number holds F /// f = F /// {f}; theorem Th223: :: MEMBER_1:223 for G being ext-real-membered set for g, f being ext-real number st g in G holds g / f in G /// f proof let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds g / f in G /// f let g, f be ext-real number ; ::_thesis: ( g in G implies g / f in G /// f ) f in {f} by TARSKI:def_1; hence ( g in G implies g / f in G /// f ) by Th102; ::_thesis: verum end; theorem Th224: :: MEMBER_1:224 for F being ext-real-membered set for f being ext-real number holds F /// f = { (w / f) where w is Element of ExtREAL : w in F } proof let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds F /// f = { (w / f) where w is Element of ExtREAL : w in F } let f be ext-real number ; ::_thesis: F /// f = { (w / f) where w is Element of ExtREAL : w in F } thus F /// f c= { (w / f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (w / f) where w is Element of ExtREAL : w in F } c= F /// f proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F /// f or e in { (w / f) where w is Element of ExtREAL : w in F } ) assume e in F /// f ; ::_thesis: e in { (w / f) where w is Element of ExtREAL : w in F } then consider w1, w2 being Element of ExtREAL such that A1: ( e = w1 * w2 & w1 in F ) and A2: w2 in {f} "" ; consider w3 being Element of ExtREAL such that A3: w2 = w3 " and A4: w3 in {f} by A2; ( w1 * (w3 ") = w1 / w3 & w3 = f ) by A4, TARSKI:def_1; hence e in { (w / f) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w / f) where w is Element of ExtREAL : w in F } or e in F /// f ) assume e in { (w / f) where w is Element of ExtREAL : w in F } ; ::_thesis: e in F /// f then ex w being Element of ExtREAL st ( e = w / f & w in F ) ; hence e in F /// f by Th223; ::_thesis: verum end; theorem :: MEMBER_1:225 for F being ext-real-membered set for f being ext-real number for e being set st e in F /// f holds ex w being Element of ExtREAL st ( e = w / f & w in F ) proof let F be ext-real-membered set ; ::_thesis: 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 ) let f be ext-real number ; ::_thesis: for e being set st e in F /// f holds ex w being Element of ExtREAL st ( e = w / f & w in F ) let e be set ; ::_thesis: ( e in F /// f implies ex w being Element of ExtREAL st ( e = w / f & w in F ) ) F /// f = { (w / f) where w is Element of ExtREAL : w in F } by Th224; hence ( e in F /// f implies ex w being Element of ExtREAL st ( e = w / f & w in F ) ) ; ::_thesis: verum end; registration let F be empty set ; let f be ext-real number ; clusterF /// f -> empty ; coherence F /// f is empty ; end; registration let F be non empty ext-real-membered set ; let f be ext-real number ; clusterF /// f -> non empty ; coherence not F /// f is empty ; end; registration let F be ext-real-membered set ; let f be ext-real number ; clusterF /// f -> ext-real-membered ; coherence F /// f is ext-real-membered ; end; definition let A be complex-membered set ; let a be complex number ; funcA /// a -> set equals :: MEMBER_1:def 24 A /// {a}; coherence A /// {a} is set ; end; :: deftheorem defines /// MEMBER_1:def_24_:_ for A being complex-membered set for a being complex number holds A /// a = A /// {a}; theorem Th226: :: MEMBER_1:226 for A being complex-membered set for b, a being complex number st b in A holds b / a in A /// a proof let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds b / a in A /// a let b, a be complex number ; ::_thesis: ( b in A implies b / a in A /// a ) a in {a} by TARSKI:def_1; hence ( b in A implies b / a in A /// a ) by Th116; ::_thesis: verum end; theorem Th227: :: MEMBER_1:227 for A being complex-membered set for a being complex number holds A /// a = { (c / a) where c is Element of COMPLEX : c in A } proof let A be complex-membered set ; ::_thesis: for a being complex number holds A /// a = { (c / a) where c is Element of COMPLEX : c in A } let a be complex number ; ::_thesis: A /// a = { (c / a) where c is Element of COMPLEX : c in A } thus A /// a c= { (c / a) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c / a) where c is Element of COMPLEX : c in A } c= A /// a proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A /// a or e in { (c / a) where c is Element of COMPLEX : c in A } ) assume e in A /// a ; ::_thesis: e in { (c / a) where c is Element of COMPLEX : c in A } then consider c1, c2 being Element of COMPLEX such that A1: ( e = c1 * c2 & c1 in A ) and A2: c2 in {a} "" ; {a} "" = {(a ")} by Th37; then ( c1 * c2 = c1 / (c2 ") & c2 = a " ) by A2, TARSKI:def_1; hence e in { (c / a) where c is Element of COMPLEX : c in A } by A1; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c / a) where c is Element of COMPLEX : c in A } or e in A /// a ) assume e in { (c / a) where c is Element of COMPLEX : c in A } ; ::_thesis: e in A /// a then ex c being Element of COMPLEX st ( e = c / a & c in A ) ; hence e in A /// a by Th226; ::_thesis: verum end; theorem Th228: :: MEMBER_1:228 for A being complex-membered set for a being complex number for e being set st e in A /// a holds ex c being Element of COMPLEX st ( e = c / a & c in A ) proof let A be complex-membered set ; ::_thesis: 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 ) let a be complex number ; ::_thesis: for e being set st e in A /// a holds ex c being Element of COMPLEX st ( e = c / a & c in A ) let e be set ; ::_thesis: ( e in A /// a implies ex c being Element of COMPLEX st ( e = c / a & c in A ) ) A /// a = { (c / a) where c is Element of COMPLEX : c in A } by Th227; hence ( e in A /// a implies ex c being Element of COMPLEX st ( e = c / a & c in A ) ) ; ::_thesis: verum end; registration let A be empty set ; let a be complex number ; clusterA /// a -> empty ; coherence A /// a is empty ; end; registration let A be non empty complex-membered set ; let a be complex number ; clusterA /// a -> non empty ; coherence not A /// a is empty ; end; registration let A be complex-membered set ; let a be complex number ; clusterA /// a -> complex-membered ; coherence A /// a is complex-membered ; end; registration let A be real-membered set ; let a be real number ; clusterA /// a -> real-membered ; coherence A /// a is real-membered ; end; registration let A be rational-membered set ; let a be rational number ; clusterA /// a -> rational-membered ; coherence A /// a is rational-membered ; end; registration let A be real-membered set ; let F be ext-real-membered set ; let a be real number ; let f be ext-real number ; identifyA /// a with F /// f when A = F, a = f; compatibility ( A = F & a = f implies A /// a = F /// f ) ; end; theorem Th229: :: MEMBER_1:229 for A, B being complex-membered set for a being complex number st a <> 0 & A /// a c= B /// a holds A c= B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & A /// a c= B /// a holds A c= B let a be complex number ; ::_thesis: ( a <> 0 & A /// a c= B /// a implies A c= B ) assume that A1: a <> 0 and A2: A /// a c= B /// a ; ::_thesis: A c= B let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B ) assume z in A ; ::_thesis: z in B then z / a in A /// a by Th226; then ex c being Element of COMPLEX st ( z / a = c / a & c in B ) by A2, Th228; hence z in B by A1, XCMPLX_1:5; ::_thesis: verum end; theorem :: MEMBER_1:230 for A, B being complex-membered set for a being complex number st a <> 0 & A /// a = B /// a holds A = B proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & A /// a = B /// a holds A = B let a be complex number ; ::_thesis: ( a <> 0 & A /// a = B /// a implies A = B ) assume ( a <> 0 & A /// a = B /// a ) ; ::_thesis: A = B then ( A c= B & B c= A ) by Th229; hence A = B by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEMBER_1:231 for A, B being complex-membered set for a being complex number st a <> 0 holds (A /\ B) /// a = (A /// a) /\ (B /// a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds (A /\ B) /// a = (A /// a) /\ (B /// a) let a be complex number ; ::_thesis: ( a <> 0 implies (A /\ B) /// a = (A /// a) /\ (B /// a) ) assume A1: a <> 0 ; ::_thesis: (A /\ B) /// a = (A /// a) /\ (B /// a) A2: {a} "" = {(a ")} by Th37; thus (A /\ B) /// a = (a ") ** (A /\ B) by Th37 .= ((a ") ** A) /\ ((a ") ** B) by A1, Th198 .= (A /// a) /\ (B /// a) by A2 ; ::_thesis: verum end; theorem :: MEMBER_1:232 for A, B being complex-membered set for a being complex number st a <> 0 holds (A \ B) /// a = (A /// a) \ (B /// a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds (A \ B) /// a = (A /// a) \ (B /// a) let a be complex number ; ::_thesis: ( a <> 0 implies (A \ B) /// a = (A /// a) \ (B /// a) ) assume A1: a <> 0 ; ::_thesis: (A \ B) /// a = (A /// a) \ (B /// a) A2: {a} "" = {(a ")} by Th37; thus (A \ B) /// a = (a ") ** (A \ B) by Th37 .= ((a ") ** A) \ ((a ") ** B) by A1, Th199 .= (A /// a) \ (B /// a) by A2 ; ::_thesis: verum end; theorem :: MEMBER_1:233 for A, B being complex-membered set for a being complex number st a <> 0 holds (A \+\ B) /// a = (A /// a) \+\ (B /// a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds (A \+\ B) /// a = (A /// a) \+\ (B /// a) let a be complex number ; ::_thesis: ( a <> 0 implies (A \+\ B) /// a = (A /// a) \+\ (B /// a) ) assume A1: a <> 0 ; ::_thesis: (A \+\ B) /// a = (A /// a) \+\ (B /// a) A2: {a} "" = {(a ")} by Th37; thus (A \+\ B) /// a = (a ") ** (A \+\ B) by Th37 .= ((a ") ** A) \+\ ((a ") ** B) by A1, Th200 .= (A /// a) \+\ (B /// a) by A2 ; ::_thesis: verum end; theorem Th234: :: MEMBER_1:234 for A, B being complex-membered set for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a) let a be complex number ; ::_thesis: (A ++ B) /// a = (A /// a) ++ (B /// a) thus (A ++ B) /// a = (a ") ** (A ++ B) by Th37 .= ((a ") ** A) ++ ((a ") ** B) by Th208 .= (A /// a) ++ ((a ") ** B) by Th37 .= (A /// a) ++ (B /// a) by Th37 ; ::_thesis: verum end; theorem :: MEMBER_1:235 for A, B being complex-membered set for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a) proof let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a) let a be complex number ; ::_thesis: (A -- B) /// a = (A /// a) -- (B /// a) thus (A -- B) /// a = (A /// a) ++ ((-- B) /// a) by Th234 .= (A /// a) -- (B /// a) by Th94 ; ::_thesis: verum end;